This course provides an introduction to the foundations, methods, and tools for automatic verification of computer systems, in particular software. Its goal is to acquaint the students with fundamentals of automatic verification and to prepare them for conducting research in the area. The focus will be on algorithmic (including model checking) methods. A separate complementary course entitled “Software Specification and Verification” covers deductive methods.

• 6/23: belated slides for Automata-Theoretic Approach available
• 6/22: slides for Compositional Reasoning and Infinite-State Systems available
• 5/23: slides for Bounded Model Checking available
• 5/19: slides for Equivalences and Abstraction and for SAT Solving available
• 5/18: Homework Assignment #1 and Homework Assignment #2 due May 27
• 5/18: slides for Symbolic Model Checkers and the SPIN Model Checker available
• 4/20: slides for mu-Calculus available
• 4/9: slides for Symbolic Model Checking available
• 3/19: slides for BDDs revised
• 3/18: slides for Ordered Sets and BDDs available
• 3/9: slides for Temporal Logic Model Checking available
• 2/24: slides for Introduction and Systems Modeling available

Yih-Kuen Tsay (蔡益坤), Room 1108, Management II, 3366-1189, Xtsay@im.ntu.edu.twX (between the enclosing pair of X's)

Wednesday 9:10AM-12:10PM, Room 203, College of Management, Building II (when the class is small enough, we meet in the seminar room on the 11th floor)

Wednesday 1:30–2:30PM (Room 1108, Management II) or by appointment

1. Model Checking, E.M. Clarke, O. Grumberg, and D.A. Peled, The MIT Press, 1999. [CGP]
2. Principles of Model Checking, C. Baier and J.-P. Katoen, The MIT Press, 2008. [BK]
3. The SPIN Model Checker: Primer and Reference Manual, G.J. Holzmann, Addison-Wesley, 2003. [H]
4. Temporal Verification of Reactive Systems: Safety, Z. Manna and A. Pnueli, Springer, 1995. [MP]
5. Selected Papers. [SP]
6. Class Notes. [CN]

We shall seek a balance between breadth and depth, covering both the foundations and some of the more successful methods and tools. Below is a tentative list of topics and their schedule:

• Introduction [CGP: Ch. 1; BK: Ch. 1; H: Ch. 1] (.5 week: 2/18a) [slides]
• Systems Modeling [CGP: Ch. 2; BK: Ch. 2,3; H: Ch. 2; MP: Ch. 0.1-4] (.5 week: 2/18b) [slides]
• Temporal Logic Model Checking [CGP: Ch. 3,4; BK: Ch. 6; MP: Ch. 5.2-3] (2 weeks: 2/25, 3/4) [slides]
• Ordered Sets and Fixpoints [CN] (1 week: 3/11) [slides]
• Binary Decision Diagrams [CGP: Ch. 5; SP] (1 week: 3/18) [slides]
• Symbolic Model Checking [CGP: Ch. 6] (1 week: 3/25) [slides]
• Model Checking μ-Calculus [CGP: Ch. 7] (1 week: 4/1) [slides]
• Symbolic Model Checkers [CGP: Ch. 8; SP; CN] (1 week: 4/8) [slides]
• Automata-Theoretic Approach [CGP: Ch. 9; BK: Ch. 4.3,4.4,5; H: Ch. 6; MP: Ch. 5.1] (1 week: 4/15) [slides]
• The Spin Model Checker [H: Ch. 3, 4, 7, 12] (1 week: 4/22) [slides]
• Partial Order Reduction [CGP: Ch. 10; BK: Ch. 8] (1 week: 4/29) (cancelled to leave time for other topics)
• Equivalences and Abstraction [CGP: Ch. 11,13; BK: Ch. 7; SP] (1 week: 5/6) [slides]
• Satisfiability Solving and Tools [SP; CN] (1 week: 5/13) [slides]
• Bounded Model Checking [SP] (1 week: 5/20) [slides]
• Final (2009/05/27)
• Satisfiability Modulo Theories (SMT), Solvers, and Applications [SP; CN] (1 week: 6/3)
• Compositional Reasoning [CGP: Ch. 12; SP; CN] (1 week: 6/10) [slides]
• Infinite-State Systems [CGP: Ch. 15; SP] (1 week: 6/17) [slides]

Homework Assignments 20%, Final Exam 40%, Term Paper/Report 40%.

Ming-Hsien Tsai (蔡明憲), 3366-1205, Xmhtsai208@gmail.comX (between the enclosing pair of X's).