15–414/614 Bug Catching: Automated Program Verification

Course Syllabus

Following is the list of topics that we intend to cover in the course. The emphasis of the course is on effective use of verification tools. We hope that at the end of the course, students will be able to do research in this area.

First Half (Interactive Theorem Proving)

  • Overview of Interactive Theorem Proving
  • Proof Assistant Coq
    • Input language - arithmetic, lists, inductive types, recursion, etc.
    • Manual proofs
    • Using tactics
    • Proving properties of programs

Second Half (Model Checking)

  • Overview of Model Checking
  • Davis Putnam procedure, fast SAT solvers
  • Binary Decision Diagrams (BDDs)
  • Property specification using Computation Tree Logic (CTL)
  • Linear temporal logic (LTL)
  • LTL model checking
  • Explicit state model checking
  • Partial order reduction
  • Symbolic model checking
  • Detailed introduction to model checker SMV
  • Detailed introduction to model checker SPIN
  • Abstract interpretation
  • Predicate abstraction and abstraction refinement
  • Detailed introduction to model checker CBMC
  • Compositional model checking