Computer Aided Verification

Spring 2006

Instructors:

Lectures: Tom Henzinger
Exercises: Nir Piterman

Schedule:

Tuesday, 10:15-11:45, INM202: Lecture
Thursday, 12:30-14:00, BC01: Lecture
Friday, 12:30-14:00, BC01: Exercises

Contact: One can send messages to all course participants using the mailing list cav06_at_listes_dot_epfl...
Instructions on how to use the mailing list are available in English and French.

Objectives: The participants will become familiar with both the theory and practice of model checking.

Motivation: Model checking concerns the use of algorithmic methods in the temporal safety and performance assurance for software and hardware systems. As our daily lives depend increasingly on digital systems, the reliability of these systems becomes a concern of overwhelming importance, and as the complexity of the systems grows, their reliability can no longer be sufficiently controlled by the traditional approaches of testing and simulation.

Syllabus:

Reactive modules: a formal model for concurrent reactive systems with software and hardware components.
Verification algorithms: linear and branching temporal logics, omega automata, equivalences and refinement, games.
State explosion: symbolic data structures, automatic abstraction, compositional reasoning.
Advanced topics: safety-liveness hierarchy, real-time and hybrid systems, probabilistic systems.

Prerequisites: The course is open to masters and doctoral students. Familiarity with propositional logic, finite automata, basic computational complexity classes, and basic graph algorithms is assumed. For example, you should know what a tautology is, how to determinize a finite automaton, what PSPACE stands for, and how to find the strongly connected components of a graph. If you are not familiar with these concepts, please see the instructor.

Lecture notes:

Chapter 0: Introduction
Chapter 1: Reactive Modules
Chapter 2: Invariant Verification
Chapter 3: Symbolic Graph Search
Chapter 4: Graph Minimization
Chapter 5: Real-Time Modules
Chapter 6: Safe Temporal Logic
Chapter 7: Safety Automata
Chapter 8: Refinement Verification
Chapter 9: Fair Modules
Chapter 10: Response Verification
Chapter 11: Live Temporal Logic
Chapter 12: Liveness Automata
Chapter 13: Linear Temporal Logic
Chapter 99: Notation

Software: Some of the homework problems will involve experimentation with the verification tool Mocha and possibly others. .

Homework: There will be weekly problem sets. Some of the homework problems will involve formal proofs, and other homework problems will involve experimentation with verification tools. The problem sets will be given on this web page every Tuesday afternoon and are due on the following Tuesday at the beginning of the lecture (10:15 am).

Quizzes: Every second Thursday there will be a 30 minute written quiz at the beginning of the lecture (10:15 am). The dates of the quizzes are:

March 30
April 13
May 4 (April 14-23 Easter)
May 18
June 8 (May 25 is Ascention day)
June 22

Mini-projects: Every student is supposed to complete a mini-project. A list of suggested mini-projects is available here. Suggestions for designing your own mini-projects according to your interests are very welcome (e.g., adapting published results to reactive modules, application of other external verification tools). The time-line for mini-projects is:

by May 18: choose the mini-project
by June 1: hand-in a 1 page summary of what you plan to do for the project
by June 29: hand-in a 5 page write-up of the project
on June 29: give a 15 minute presentation of the project

Grading: Grades will be awarded on the basis of attending exercises, performance on quizzes, performance on homework, and performance on the mini-project. Every attended exercise will yield 2 points, up to a possible maximum of 20 points. Every quiz will yield a maximum of 5 points, and the best 4 out of the 6 quizzes are counted, for a total maximum of 20 points. Every homework will yield a maximum of 4 points, and the best 10 out of the 13 homeworks are counted, for a total maximum of 40 points. At exercise, you may be asked to present your solutions to the previous homework. If the presenter does not understand his/her own solution, the homework may be graded as 0 points, and the maximum number of points achievable through homework may be decreased by 4 points. The write-up and presentation of the mini-project will yield a maximum of 20 points. There will be no final exam. Excuses for missing exercises, quizzes, or homeworks will not be accepted.

Summary:

exercise attendance: 20 points
quizzes (4 out of 6): 20 points
homeworks (10 out of 13): 40 points
mini-project: 20 points

Teamwork: Students may collaborate on homeworks, but each student needs to individually write up a solution set and be prepared to present it during exercises. Mini-projects must be done individually, or as clearly identifiable parts of a larger effort with individual write-ups and presentations.