Computer Aided Verification
2004
Instructors:
Schedule:
- Tuesday, 10:15-11:45, INM201: Lecture
- Thursday, 11:15-12:45, INM201: Lecture
- Thursday, 14:15-15:45, INM201: Exercises
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: 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.
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).
- Oct 26: Download and install jMocha
(Version 2.0) on your computer. Study Peterson's mutual exclusion
protocol which is explained in jMocha's user guide on pages 14-15. Use
the reactive module definitions which are given in the distribution's
example directory. Verify the mutual exclusion property and generate
one simulation trace. Hand-in your specification of the mutual
exclusion property, the verification results, and the simulation trace
you get from Mocha.
- Nov 2: Exercise 1.5: Classification of modules, and Exercise
1.7: Synchronous circuits, and Exercise 1.13: Dining Philosophers. All
from the lecture notes, chapter 1.
- Nov 9: Exercise 2.3: Transition graph of compound modules,
and Exercise 2.5: Railroad control, and Exercise 2.7: Mutual exclusion,
and Exercise 2.10: Nonrecursive depth-first reachability checking. All
from the lecture notes, chapter 2.
- Nov 16: Exercise 2.18: Latch-reduced transition graph for
railroad control, and Exercise 2.23: Composing invariants, and Exercise
3.1: Fixpoint view of breadth-first search, and Exercise 3.3: Witness
reporting in symbolic search
- Nov 23: Exercises 4.3, 4.7, and 4.14.
- Nov 30: Exercise 3.12: Representation using BDDs, and
Exercise 3.13: Exponential dependence on variable-ordering, and
Exercise 3.21: Substitution in BDDs, and Exercise 5.2: Region graph
- Dec 7: Exercise 5.10: Difference-bound matrices (DBMs),
Only: Give an algorithm for computing timepre, what is the cost of the
operation, and Exercise 6.1: Weak equivalence of state formulas, and
Exercise 6.12: Symbolic region difference.
- Dec 14: Exercise 6.20: Stutter-intensive bisimilarity, and Exercise 6.21: STL-until, and Exercise 7.2: Mutual exclusion
- Dec 21: Exercise 7.3: Specifying formula in SAL, and Exercise
7.11: Operations on automata, and Exercise 8.3: Synchronous vs.
asynchronous message passing
- Jan 11: Exercise 8.11: Backward simulation, and Exercise
8.16: Synchronous vs. asynchronous message passing, and Exercise 8.22:
Weak similarity vs. trace equivalence.
- Jan 18: Exercise 9.1: Safety verification, and Exercise 9.2:
'safe' does not distribute over union, and Exercise 9.5 {T2}:
Obligation languages
- Jan 25: Exercise 9.16: Intersection and machine closure, and
Exercise 9.21: Fair dining philosophers, and Exercise 10.4: Dining
philosophers.
- Feb 1: Exercise 10.9: Fair regions, and Exercise 11.6: Non-compositionality of CTL, and Exercise 11.14: Formula in mu-Calculus.
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:
- November 4
- November 18
- December 2
- December 16
- January 13
- January 27
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:
- by December 9: choose the mini-project
- by December 23: hand-in a 1 page summary of what you plan to do for the project
- by February 3: hand-in a 5 page write-up of the project
- on February 3: 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
accepted.
Summary:
- 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.
Lecture 1 (October 19):
- What is model checking?
- Recent successes in hardware and software verification
- Modeling languages
Lecture 2 (October 21):
- The modeling language Reactive Modules
- Operations on Reactive Modules
Lecture 3 (October 26):
- Modeling synchronous circuits
- Modeling shared-memory processes
- Modeling message-passing processes
Lecture 4 (October 28):
- Transition graphs
- From Reactive Modules to transition graphs
Lecture 5 (November 2):
- Invariant verification
- Monitors
- Explicit state search
Lecture 6 (November 4):
- Hardness of verification
- On-the-fly search
Lecture 7 (November 9):
- Assume-guarantee verification
- Symbolic search
Lecture 8 (November 11):
- Abstraction
- Stable partitions
- Symmetry reduction
Lecture 9 (November 11):
- Partition refinement
- Paige-Tarjan? algorithm
Lecture 10 (November 18):
- Binary decision diagrams
- BDD operations
Lecture 11 (November 23):
- Real-time modules
- Clock constraints
Lecture 12 (November 25):
- Clock regions
- Difference-bound matrices
Lecture 13 (November 30):
- State logics
- Safe temporal logic
- STL model checking
Lecture 14 (December 2):
- State equivalences
- Bisimilarity
Lecture 15 (December 7):
- STL induces bisimilarity
- STL expressiveness
Lecture 16 (December 9):
- Safe automaton logic
- Operations on automata
Lecture 17 (December 14):
- SAL model checking
- State preorders
- Similarity
Lecture 18 (December 16):
- Similarity checking
- SAL induces trace equivalence
- SAL expressiveness
Lecture 19 (December 21):
- Symbolic similarity checking
- Drifting clocks
- Compositional refinement checking
Lecture 20 (December 23):
- Assume-guarantee reasoning
- Safety vs. liveness
Lecture 21 (January 11):
- The safety-progress hierarchy
- Weak and strong fairness
Lecture 22 (January 13):
- Fair graphs
- Fair modules
- Receptiveness
Lecture 23 (January 18):
- Response verification
- Strongly connected components
- Weakly fair emptiness
Lecture 24 (January 20):
- Strongly fair emptiness
- CTL
Lecture 25 (January 25):
- The mu-calculus
- Expressive power of the mu-calculus
- Symbolic model checking for the mu-calculus
Lecture 26 (January 27):
- Automata over infinite words
- The omega-regular languages
Lecture 27 (February 1):
- Linear temporal logic
- Tableau construction
Lecture 28 (February 3):
- The state and future of model-checking research
- Class project presentations