Logo EPFL
I&C
Ecole Polytechnique Fédérale de Lausanne
Model Checking 2007
english only

Model Checking

Winter 2007





Instructors:



Schedule:



Contact: Participants are asked to subscribe to the mailing list modelchecking2007_at_listes_dot_epfl_dot_ch to allow one to send messages to all course participants. Instructions on how to subscribe and 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:



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:



Exercises

Software: Some of the homework problems will involve experimentation with the verification tool Mocha. Please find some notes on how to install and use Mocha here.



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 Thursday afternoon and are due on the following Thursday at the beginning of the lecture.

Quizzes: Every second Tuesday there will be a 30 minute written quiz at the beginning of the lecture (14:15). 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.



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.



Topic Summary of Lectures



Sep 18 Sep 20 Sep 25 Sep 27 Oct 2 Oct 4 Oct 9 Oct 11 Oct 16 Oct 18 Oct 23 Oct 25 Oct 30 Nov 1 Nov 6 Nov 8 Nov 13 Nov 15 Nov 20 Nov 22 Nov 27 Nov 29 Dec 4 Dec 6 Dec 11 Dec 13 Dec 18 Dec 20
Update now