Logo EPFL
I&C
Ecole Polytechnique Fédérale de Lausanne
CAV 2004
english only

Computer Aided Verification

2004



Instructors:

Schedule:

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:

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 tools Mocha and Blast.

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 (11:15 am). The dates of the quizzes are:

Mini-projects: Every student is supposed to complete a mini-project. Potential mini-project topics, both theoretical and experimental, will be announced during the course. Typical mini-projects will involve the summary and minor modification of a research article, say by adapting published results to the formalism of reactive modules; or the installation of an external verification tool and its application to one of our examples. Any suggestions for designing your own mini-project according to your interests are very welcome. 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.
Summary:

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.

Lecture 1 (October 19):

Lecture 2 (October 21):

Lecture 3 (October 26):

Lecture 4 (October 28):

Lecture 5 (November 2):

Lecture 6 (November 4):

Lecture 7 (November 9):

Lecture 8 (November 11):

Lecture 9 (November 11):

Lecture 10 (November 18):

Lecture 11 (November 23):

Lecture 12 (November 25):

Lecture 13 (November 30):

Lecture 14 (December 2):

Lecture 15 (December 7):

Lecture 16 (December 9):

Lecture 17 (December 14):

Lecture 18 (December 16):

Lecture 19 (December 21):

Lecture 20 (December 23):

Lecture 21 (January 11):

Lecture 22 (January 13):

Lecture 23 (January 18):

Lecture 24 (January 20):

Lecture 25 (January 25):

Lecture 26 (January 27):

Lecture 27 (February 1):

Lecture 28 (February 3):