Course Outline

OBJECTIVE and DESCRIPTION:

Please note that this course is cross listed with CMPT 773

Real software systems are extremely complex. In the software industry, formal verification methods are increasingly used to verify that a model of a software system satisfies the requirements. The course concentrates on contemporary applications of logic to the verification of software systems. The objective is to introduce, at an accessible level, a mathematical framework for symbolic model checking, one of the most important verification methods. The techniques are illustrated with examples of verification of reactive systems and communication protocols. Students learn to work with the model checking tool SMV.

TOPICS:

• model checking as a verification technique
• model checking with Computational Tree Logic (CTL)
• representing practically relevant specifications in CTL
• the NuSMV (``symbolic model verifier'') system
• alternatives and extensions of CTL
• model checking with fairness
• efficient representation of boolean functions - binary decision diagrams
• use of binary decision diagrams in symbolic model checking
• model checking for the relational mu-calculus

GRADING:

• Four assignments (paper-pencil and programming): 40%
• Midterm: 20 %
• Final Exam: 40 %

TEXTBOOKS: Logic in Computer Science: Modelling and Reasoning about Systems, Michael R. A. Huth and Mark D. Ryan, Cambridge University Press, 2nd edition.

REFERENCES: Model Checking, E. M. Clarke, O. Grumberg and D. Peled, MIT Press, 2000