Computer Aided Verification
Spring 2006
Instructors:
Schedule:

Tuesday, 10:1511:45,
INM202: Lecture

Thursday, 12:3014:00,
BC01: Lecture

Friday, 12:3014: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: safetyliveness hierarchy, realtime 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:
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 1423 Easter)
 May 18
 June 8 (May 25 is Ascention day)
 June 22
Miniprojects: Every student is supposed to complete a
miniproject. A list of suggested miniprojects is available here.
Suggestions for designing your own miniprojects according to your
interests are very welcome (e.g., adapting published results to reactive
modules, application of other external verification tools).
The timeline for miniprojects is:
 by May 18: choose the miniproject
 by June 1: handin a 1 page summary of what you plan to do
for the project
 by June 29: handin a 5 page writeup 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 miniproject. 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 writeup and presentation of the
miniproject 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
 miniproject: 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. Miniprojects must be done
individually, or as clearly identifiable parts of a larger effort with
individual writeups and presentations.