Overview

Description

CALENDAR DESCRIPTION:

Introduces, at an accessible level, a formal 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 a model checking tool.

COURSE DETAILS:

(Please note that this course is cross-listed with CMPT 777)

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

Materials

REQUIRED READING: