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.

• Model Checking
  • Symbolic Model Checking with BDDs
  • Symbolic Model Checking with SAT
    • Bounded Model Checking
    • Unbounded Model Checking
  • Counterexample guided abstraction refinement
  • How to use the SMV model Checker
• Fast SAT procedures
• Grasp
• Chaff
• How to use Chaff
• PVS
  • How to use it
    • Basic language
    • More on types
    • Proofs
  • How it works
• Combining Model Checking and Theorem Proving
• HOL / Isabelle (if time permits)

Subject to Change - check page frequently