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
• Property specification using Computation tree logic (CTL)
• Concurrency
• Explicit state model checking
• Fairness
• Binary Decision Diagrams (BDDs)
• Symbolic model checking
• Detailed introduction to model checker SMV
• Linear temporal logic (LTL)
• LTL tableaux construction
• LTL model checking
• Detailed introduction to model checker SPIN

• Program Testing
• SAT based model checking
• Abstraction and compositional reasoning
• Hoare logic and sequential programs
• Automated theorem proving

Subject to Change.