The goal of this course is to acquaint the students with fundamentals of automatic verification (of computer systems, in particular software) and to prepare them for conducting research in the area.

• 01/19: grade report available; please send inquiries, if any, to the instructor by 2PM 01/20.
• 12/18: old exams.
• 12/18: slides for Bounded Model Checking available.
• 12/11: slides for Satisfiability Solving and Tools available.
• 12/04: slides for Compositional Reasoning available.
• 11/27: slides for Equivalence, Simulation, and Abstraction available.
• 11/20: slides for SPIN available.
• 11/20: HW#6 due on 11/27.
• 11/05: HW#5 due on 11/13.
• 11/05: slides for Automata-Theoretic Approach and for An Example available.
• 10/30: slides for Symbolic Model Checkers available.
• 10/24: the diagram in Problem 3 of HW#4 corrected.
• 10/23: slides for Model Checking mu-Calculus available.
• 10/23: HW#4 due on 10/30.
• 10/15: slides for Symbolic Model Checking available.
• 10/09: HW#3 due on 10/16.
• 10/09: slides for Binary Decision Diagrams available.
• 10/02: slides for Ordered Sets and Fixpoints available.
• 10/02: HW#2 due on 10/09.
• 09/18: slides for Temporal Logic Model Checking available.
• 09/18: HW#1 due on 09/25.
• 09/11: slides for Introduction and for Systems Modeling available.
• 09/03: this website created on 08/31.

Yih-Kuen Tsay (蔡益坤), NTU IM Dept., 3366-1189, Xtsay@im.ntu.edu.twX (between the enclosing pair of X's)

Wednesday 2:20–5:20PM, Room 203, Management Building 1 (when the class is small enough, we meet in the seminar room on the 11th floor)

Tuesday 1:30–2:00PM, Wednesday 1:30–2:00PM, or by appointment, Room 1108, Management II

1. Model Checking, E.M. Clarke, O. Grumberg, and D.A. Peled, The MIT Press, 1999. [CGP](A copy of this book has been put on reserve at NTU Library in the 教師指定參考書區 under the name “BM-5自動化軟體驗證”.)
2. Principles of Model Checking, C. Baier and J.-P. Katoen, The MIT Press, 2008. [BK] (A copy of this book has also been put on reserve at NTU Library.)
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]

This course provides an introduction to the foundations, methods, and tools for automatic verification. The focus is on algorithmic (including model checking) methods. A separate complementary course entitled “Software Specification and Verification” covers deductive methods. 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: 9/11a) [slides]
• Systems Modeling [CGP: Ch. 2; BK: Ch. 2,3; H: Ch. 2; MP: Ch. 0.1-4] (.5 week: 9/11b) [slides]
• Temporal Logic Model Checking [CGP: Ch. 3,4; BK: Ch. 6; MP: Ch. 5.2-3] (2 weeks: 9/18, 9/25) [slides]
• Ordered Sets and Fixpoints [CN] (1 week: 10/2) [slides]
• Binary Decision Diagrams [CGP: Ch. 5; SP] (1 week: 10/9) [slides]
• Symbolic Model Checking [CGP: Ch. 6] (1 week: 10/16) [slides]
• Model Checking μ-Calculus [CGP: Ch. 7] (1 week: 10/23) [slides]
• Symbolic Model Checkers [CGP: Ch. 8; SP; CN] (1 week: 10/30) [slides]
• Automata-Theoretic Approach [CGP: Ch. 9; BK: Ch. 4.3,4.4,5; H: Ch. 6; MP: Ch. 5.1] (2 weeks: 11/6, 11/13) [slides: Automata-Theoretic Approach to Model Checking, An Example of Temporal Formula to Automaton Translation]
• The Spin Model Checker [H: Ch. 3, 4, 7, 12] (1 week: 11/20) [slides]
• Equivalence, Simulation, and Abstraction [CGP: Ch. 11,13; BK: Ch. 7; SP] (1 week: 11/27) [slides]
• Compositional Reasoning [CGP: Ch. 12; SP; CN] (1 week: 12/4) [slides]
• Satisfiability Solving and Tools [SP; CN] (1 week: 12/11) [slides]
• Bounded Model Checking [SP] (1 week: 12/18) [slides]
• Final (2019/12/25)
• Wrap-Up Discussions (1 week: 2020/1/8)

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