Vanderbilt University · College of Connected Computing
A hands-on four-day short course on proving software and systems correct — and on how AI is changing that practice.
Each day builds one pillar of the modern verification toolkit and applies it to a shared set of running examples: SAT/SMT solving, model checking, interactive theorem proving, and program & high-assurance verification — closing on the AI frontier (neural-network verification and AI-assisted proof). Every idea ships with runnable code, and everything below runs in the browser with no local install.
In a deck: arrow keys navigate, S speaker notes, F fullscreen, Esc the slide grid.
New to these tools? Start with the Day 0 setup slides or the step-by-step Getting Started guide — then pick a path below.
.smv files.examples/ and assignments/, and a capstone that runs one property through all four tools.