Office Hours:

Tues: 2:30 - 4:00,

Wed: 2:00 - 3:30,

and by appointment

In the first three classes, I gave an introduction to model checking and then a review and summary of predicate logic, and first-order logic. Here is Homework 1, due Wednesday, Sept. 22.

We have introduced the syntax and semantics of LTL, CTL, and CTL* and started using the NuSMV model checker. Here is Homework 2, due Wednesday, Oct. 6.

We have shown how to do explicit model checking of CTL and Fair CTL. Then we showed how to translate an LTL specification, ϕ, into a Buchi automaton of size at most 2^|ϕ| size. We can combine this Buchi automaton with the original Kripke structure, and understand the Buchi acceptance conditions as fairness conditions. Thus we can check the LTL formula using Fair CTL model checking.

On Monday, Oct. 18, we introduced the mu-calculus and showed that CTL and more can be expressed. On Wednesday, Oct. 20, we explained the basic properties of OBDDs. Here is Homework 3, due Wednesday, Oct. 27.

The week of Nov. 1, I started talking about abstraction by presenting the following paper:

Sagiv, M., Reps, T., and Wilhelm, R., Parametric shape analysis via 3-valued logic. In ACM Transactions on Programming Languages and Systems 24, 3 (2002), 217-298. [PDF; Powerpoint].

On Monday, Nov. 8 I talked about the paper: Lazy Abstraction by Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre , Proceedings of the 29th Annual Symposium on Principles of Programming Languages (POPL), ACM Press, 2002, pp. 58-70. This is the theoretical basis of the BLAST software model-checking system.

Final Projects Presentation Schedule

• Mon, Dec 6
  • Jianbin Tan, "Using ZBDD's in a SAT Solver"
  • Nathan Jokel, "Applying the FLAVERS Model Checker to Infinite Program Executions"
  • Shangzhu Wang, "Compositional model checking"
• Wed. Dec 8
  • Frank Otto, "Approaches and methods of program verification"
  • Richard Chang, "Checking consistency for sets of properties"
  • Siddharth Srivastava, "Model Checking of Probabilistic Systems"
• Fri, Dec 10
  • Philipp Weis "Complexity of Mu-Calculus Model-Checking"
  • Yao Chen, "Process Language Analysis by Model Checking: a Case Study on Blood Transfusion"
  • Bin Chen, "Software model checking"
• Mon, Dec 13
  • Martin Allen, "Model checking knowledge-based systems with inconsistency."