Yih-Kuen Tsay's Wiki @ IM.NTU

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Automatic Verification, Spring 2010 ======
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.

===== Announcements =====
  * 6/03: slides for SAT Solving and Tools available
  * 5/26: slides for Compositional Reasoning available
  * 5/26: {{courses:av2010:hw2.pdf|HW#2}} due on June 9
  * 5/19: slides for Equivalences and Abstraction available
  * 5/19: slides for SPIN available
  * 5/18: slides and note for Symbolic Model Checkers available
  * 4/28: slides for Automata-Theoretic Approach available
  * 4/21: slides for Model Checking mu-Calculus available
  * 4/13: {{courses:av2010:hw1.pdf|HW#1}} due on April 21
  * 3/24: slides for Binary Decision Diagrams available
  * 3/20: slides for Ordered Sets and Fixpoints available
  * 3/03: slides for Temporal Logic Model Checking available
  * 2/24: {{courses:av2010:av2010info.pdf|PDF version}} of this page (as of 2010/02/24, without the announcements)
  * 2/19: slides for Introduction and Systems Modeling available

===== Instructor =====

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

===== Lectures =====

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

===== Office Hours =====

Wednesday 1:30--2:30PM or by appointment, Room 1108, Management II

===== Textbooks =====

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

===== Syllabus/Schedule (with links to slides/notes)=====
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: 2/24a) [{{courses:av2010:introduction.pdf|slides}}]
  * Systems Modeling [CGP: Ch. 2; BK: Ch. 2,3; H: Ch. 2; MP: Ch. 0.1-4] (.5 week: 2/24b)   [{{courses:av2010:modeling.pdf|slides}}]
  * Temporal Logic Model Checking [CGP: Ch. 3,4; BK: Ch. 6; MP: Ch. 5.2-3] (2 weeks: 3/3, 3/10) [{{courses:av2010:temporal_logic_model_checking.pdf|slides}}]
  * Ordered Sets and Fixpoints [CN] (1 week: 3/17) [{{courses:av2010:ordered_sets.pdf|slides}}]
  * Binary Decision Diagrams [CGP: Ch. 5; SP] (1 week: 3/24) [{{courses:av2010:bdd.pdf|slides}}]
  * Symbolic Model Checking [CGP: Ch. 6] (1 week: 3/31) [{{courses:av2010:symbolic_model_checking.pdf|slides}}]
  * Model Checking μ-Calculus [CGP: Ch. 7] (1 week: 4/14) [{{courses:av2010:mu_calculus.pdf|slides}}]
  * Symbolic Model Checkers [CGP: Ch. 8; SP; CN] (1 week: 4/21) [{{courses:av2010:symbolic_model_checkers.pdf|slides}}; [{{courses:av2010:nusmv_cmd.pdf|note}}]
  * Automata-Theoretic Approach [CGP: Ch. 9; BK: Ch. 4.3,4.4,5; H: Ch. 6; MP: Ch. 5.1] (1 week: 4/28)  [{{courses:av2010:automata_theoretic_approach.pdf|slides}}]
  * The Spin Model Checker [H: Ch. 3, 4, 7, 12] (1 week: 5/5) [{{courses:av2010:the_spin_model_checker.pdf|slides}}]
  * Equivalences and Abstraction [CGP: Ch. 11,13; BK: Ch. 7; SP] (1 week: 5/12) [{{courses:av2010:abstraction.pdf|slides}}]
  * Compositional Reasoning [CGP: Ch. 12; SP; CN] (1 week: 5/19) [{{courses:av2010:compositional_reasoning.pdf|slides}}]
  * Satisfiability Solving and Tools [SP; CN] (1 week: 5/26) [{{courses:av2010:sat.pdf|slides}}]
  * Bounded Model Checking [SP] (1 week: 6/2) [{{courses:av2010:bounded_model_checking.pdf|slides}}]
  * **Final** (**2010/06/09**)
  * Satisfiability Modulo Theories (SMT), Solvers, and Applications [SP; CN] (1 week: 6/23) [{{courses:av2010:smt.pdf|slides}}]

===== Grading =====

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

===== TA =====

Chih-Pin Tai (戴智斌), 3366-1205, ''Xsteve750312@gmail.comX'' (between the enclosing pair of X's).
Yih-Kuen Tsay's Wiki @ IM.NTU

User Tools

Site Tools

Page Tools
