CS 294-1: Model Checking
EE 219C: Computer-Aided Verification
Spring 2003
Lecture 1 (January 21):
- What is model checking?
- Recent successes in hardware and software verification
"This has been the Holy Grail of computer science for many decades,
but now in some very key areas, for example, driver verification, we're
building tools that can do actual proof about the software and how it
works in order to guarantee the reliability."
Bill Gates, April 18, 2002, Keynote address at WinHEC 2002.
- State space models: The modeling language Reactive Modules
Notes:
Some Notation
Notes:
Reactive Modules
Lecture 2 (January 23):
- Dependency relations between atoms
- Trajectories and traces
- Synchronous vs. asynchronous modules
- Operations on reactive modules
Problem Set 1 (due January 30; graders C. Karlof and T. Terauchi):
- Problems 1.7, 1.11, and 1.13.
- Start up jMocha
(Version 2.0) and have it parse some of the reactive modules you give as
answers to the previous question.
Lecture 3 (January 28):
- Synchronous circuits
- Control flow graphs of multi-threaded programs
- Synchronous message passing
- Real time
Notes:
Invariant Verification
Lecture 4 (January 30):
- State transition graphs
- From reactive modules to transition graphs
- Invariant verification as graph reachability
- Monitors
Problem Set 2 (due February 6; grader A. Davare):
- Problems 1.16(a)-(b), 2.3, 2.5, and 2.7.
- Use jMocha to solve an invariant verification problem of your choice
(e.g., a mutex protocol).
Lecture 5 (February 4):
- Depth-first search
- Enumerative verification
- Optimizations
Lecture 6 (February 6):
- State explosion
- Compositional verification
- Assume-guarantee reasoning
Problem Set 3 (due February 13; graders S. Matic and W. Plishker):
- Problems 2.19, 2.23, and 2.25 (assume-guarantee part only).
Lecture 7 (February 11):
- Region algebra
- Symbolic search
- Binary decision diagrams
Notes:
Symbolic Graph Representation
Lecture 8 (February 13):
- Operations on BDDs
- Abstraction
- Stable partitions
Problem Set 4 (due February 20; graders D. Nguyen and J. Kodumal):
- Problems 3.1, 3.3, 3.13, and 3.16.
Notes:
Graph Minimization
Lecture 9 (February 18):
- Variable abstractions
- Graph symmetries
- Partition refinement
Lecture 10 (February 20):
- Paige-Tarjan algorithm
- Real-time modules
- Clock regions
Problem Set 5 (due February 27; graders S. Chatterjee and D. Densmore):
- Problems 4.3, 4.12, 4.14, and 5.6.
Notes:
Real-Time Modules
Lecture 11 (February 25)
[guest lecturers Ranjit Jhala and Rupak Majumdar]:
- Predicate abstraction
- Counterexample-guided abstraction refinement
- BLAST
Lecture 12 (February 27)
[guest lecturer Orna Kupferman]:
- Safe temporal logic
- STL model checking
Problem Set 6 (due March 6; graders Y. Li and G. Yang):
- Problems 5.9, 6.4, and 6.9.
Notes:
Temporal Safety Requirements
Lecture 13 (March 4):
- State equivalences
- Bisimilarity
- Distinguishing power of STL
Lecture 14 (March 6):
- Expressive power of STL
- Safe automaton logic
- Expressive power of SAL
Problem Set 7 (due March 13; grader M. Zennaro):
- Problems 6.17, 6.23, 7.2, and 7.10.
Notes:
Automata-theoretic Safety Verification
Lecture 15 (March 11):
- Operations on automata
- Determinization of automata
- SAL model checking
Notes:
Hierarchical Verification
Lecture 16 (March 13):
- Refinement checking
- Compositional and assume-guarantee reasoning
- Language equivalence, similarity, and bisimilarity
Problem Set 8 (due March 20; graders S. Gulwani and A. Hurst):
- Problems 8.2, 8.6, 8.11, and 8.15.
Lecture 17 (March 18):
- Enumerative simulation checking
- Symbolic simulation checking
- Stuttering and weak equivalences
Notes:
Fair Modules
Lecture 18 (March 20):
- Safety vs. liveness
- Safety vs. guarantee
- The progress hierarchy
Problem Set 9 (due April 3; graders S. Goldsmith and E. Matsikoudis):
- Problems 9.1, 9.6, and 9.7.
Lecture 19 (April 1):
- Recurrence, persistence, and reactivity
- Weak and strong fairness
- Locality, machine closure, and receptiveness
Notes:
Response Verification
Lecture 20 (April 3):
- Recurrence verification and response monitors
- Strongly connected components
- The weakly-fair and strongly-fair emptiness problems
Problem Set 10 (due April 10; graders A. Chakrabarti and A. Ghosal):
- Problems 9.16, 10.3, and 10.14.
Lecture 21 (April 8):
- CTL
- Enumerative model checking for CTL
- The mu-calculus
- Symbolic model checking for the mu-calculus
Notes:
Temporal Liveness Requirements
Lecture 22 (April 10):
- Alternation-free mu-calculus
- Fairness in the mu-calculus
- Expressive power of the mu-calculus
Problem Set 11 (due April 17; grader M. Harren):
- Problems 11.3, 11.6, 11.14, and 11.16.
Notes:
Automata-theoretic Liveness Requirements
Lecture 23 (April 15):
- Omega-automata
- Operations on omega-automata
- Hierarchy of deterministic omega-automata
Notes:
Linear Temporal Logic
Lecture 24 (April 17):
- Linear temporal logic
- Expressiveness of LTL
- Tableau construction for LTL
Problem Set 12 (due May 1; graders K. Chatterjee and R. Jiang):
- Problems 12.3, 13.7, and 13.10.
Lectures 25, 26, and 27 (April 22, 24, and 29)
[guest lecturer Orna Kupferman]:
- Alternating automata
- Complementation of omega-automata
Lecture 28 (May 1):
- LTL satisfiability and model checking
- Quantified LTL and omega-automata
- CTL*
Problem Set 13 (due May 8; graders H. Zeng and Y. Li):
- Problems 13.11 and 13.12.
- Prove or give a counterexample: nondeterministic co-Buchi word
automata are as expresive as deterministic co-Buchi word automata.
(Hint: consider the Miyano-Hayashi translation from alternating to
nondeterministic Buchi word automata.)
Lecture 29 (May 6):
- S1S
- Safety and reachability games
- Concurrent games
Lecture 30 (May 8)
[guest lecturer Marcin Jurdzinski]:
Lecture 31 (May 13):
- Hybrid systems
- Polyhedral analysis
- Verification vs. control
http://www.eecs.berkeley.edu/~tah/294-1
Last updated in November, 2002, by
tah@eecs.berkeley.edu