Ecole Polytechnique Fédérale de Lausanne
CAV 2006
english only

Computer Aided Verification

Spring 2006



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.


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:

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:

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:

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.


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.