Computer Aided Verification
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
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.
- 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.
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
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
- 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.