Course site in preparation. Details below are tentative and will be updated before the semester begins.
If you are interested in the course, please fill out this google form
From tests to proofs: how do we know our software (and hardware) works?
Passing tests is useful evidence, but what does it establish, and what might it miss? This hands-on course explores the spectrum of software verification, from regression testing, AI-generated tests, and fuzzing to static analysis, symbolic execution, model checking, and machine-checked proofs. We will try tools, write specifications, investigate counterexamples, and compare the guarantees, assumptions, costs, and limitations of different approaches.
The emphasis is on software, with selected hardware examples where useful.
A course project puts these techniques in practice on an open-source codebases where students will apply multiple tools and explain what each could and could not establish.
Course communication, submission, and office-hour links will be posted here when available.
| Stage | Guiding question | Topics |
|---|---|---|
| Testing and development workflows | What evidence do our tests provide? | Unit and regression testing, coverage, test oracles, CI/CD |
| Generating tests and observing behavior | How can we find failures we did not anticipate? | Property-based and AI-generated tests, fuzzing, dynamic analysis, sanitizers |
| Analyzing programs | What can we learn without running every input? | Static analysis, specifications, assertions, invariants |
| Exploring paths and states | How can tools search for counterexamples? | Symbolic execution, SAT/SMT, model checking |
| Proving and checking properties | What does a machine-checked proof establish? | Deductive verification, proof assistants, proof checking, trust assumptions |
We plan to introduce a tool roughly every one to two weeks.
Dated sessions, readings, and materials will be posted here as the course develops.