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
Textbooks
- Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions
- Edmund M. Clarke Jr., Orna Grumberg and Doron A. Peled. Model Checking