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.
- Overview of model checking
- Quick introduction to logic
- Propositional logic
- Davis Putnam procedure, fast SAT solvers
- Binary Decision Diagrams (BDDs)
- Property specification using Computation Tree Logic(CTL)
- Linear temporal logic (LTL)
- LTL tableaux construction
- 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 abstract refinement
- Detailed introduction to model checker CBMC
- Compositional model checking
- Probabilistic model checking
- Statistical model checking
Textbooks
