Model Checking
Winter 2007
Instructors:
Schedule:

Tuesday, 14:1516:00
BC01: Lecture

Thursday, 10:1512:00
INM200: Lecture

Friday, 13:1515:00,
INM200: Exercises
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:
 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:
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:
 Oct 2
 Oct 16
 Oct 30
 Nov 13
 Nov 27
 Dec 18 (instead of Dec 11)
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 Nov 20: choose the miniproject
 by Dec 4: handin a 1 page summary of what you plan to do
for the project
 by Jan 10: handin a 5 page writeup of the project for theory
projects, and 3 page summary and the source code for implementation
projects.
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.
Topic Summary of Lectures
Sep 18
 Introduction to verification
 Introduction to Reactive Modules
Sep 20
 Definition of Reactive Modules
 Operations on Reactive Modules
Sep 25
 Modeling synchronous hardware
 Modeling multithreaded software
 From Reactive Modules to transition graphs
Sep 27
 Invariant verification and graph reachability
 Safety monitors
 Depthfirst search
Oct 2
 Symbolic graph representation
 Symbolic search
 Translation of modules to symbolic representations (initial and
update predicate)
Oct 4
 Comparison of symbolic and enumerative representations
 Space optimizations
 Hardness and complexity of invariant verification
Oct 9
 Binary Decision Diagrams
 Symbolic search with BDDs
Oct 11
 Compositional verification
 Abstraction
Oct 16
 Graph minimization
 Stable partitions
 Graph symmetries
Oct 18
 Computing stable partitions
 PaigeTarjan algorithm
Oct 23
 Reachable Partition Refinement (LeeYannakis algorithm)
 Realtime verification problem
 Realtime propositional modules
Oct 25
 Clock regions, clock constraints
 Enumerative and symbolic verification of realtime modules
 Differencebound Matrices (DBM)
Oct 30
 Safe Temporal Logic (STL)
 Observation structure (Kripke structure)
Nov 1
 Model checking STL
 Comparing state logics (expressive and distinguishing power)
 State equivalences (Bisimilarity)
Nov 6
 STL distinguishing power
 Characterization of bisimilarity
 Safe Automata Logic (SAL)
Nov 8
 Distinguishing power of SAL
 Expressive power of SAL
 Model checking SAL
Nov 13
 Model checking SAL
 Operations on automata
 Complementation of an automaton
Nov 15
 Comparison of STL and SAL
 Simulation
Nov 20
 Bisimularity versus simulation
 Refinement checking
 Assumeguarantee rule
Nov 22
 Safety versus Liveness
 Language of infinite sequences
 Definition of safe, live, and machineclosed
Nov 27
 Topology
 Fair graphs
 Streett and Büchi fairness
Nov 29
 Strong and weak fairness constraints
 Recurrence verification problem
Dec 4
 Fair ωtrajectory problem
 Strong Connected Component (SCC)
 Tarjan's algorithm
Dec 6
 Computational Tree Logic (CTL)
 CTL model checking
 Syntax and semantics of μCalculus (CTμ)
Dec 11
 CTL in CT&mu
 Model Checking CT&mu
 Expressive power of CT&mu
Dec 13
 Expressive power of CT&mu
 ωautomata
 Büchi/Streett/Rabin automata
Dec 18
 Automatatheoretic Liveness Verification
 Complementation of NBA
Dec 20
 ωregular languages
 Counterfree and not counterfree languages
 Linear Temporal Logic (LTL)
 LTL Model Checking
Update now