Model-Checking SS 2010

News | Basic information | Content | Exercises | Slides | Links

Model-Checking (also in German: Modellprüfung) is a technique for automatic verification of hardware and software systems. Given a such system and a correctness specification, a model checker checks if the system works correctly.

Textbook: We will use the survey on Software Model Checking by Ranjit Jhala and Rupak Majumdar as a basis.

Prerequisites: Basic discrete math and logic.

Lecture 1: April 19

Basic introduction.

Lecture 2: April 20

Sec. 1.1: programs, computations, post/pre/wp.
Sec. 1.2: reachability and termination properties.
Sec. 2.1: concrete enumerative stateful reachability algorithm.

Tutorial 1: April 22

Basics of set and lattice theory, logic and constraint solving.
A simple algorithm and its correctness proof: PDF and TEX.

Lecture 3: April 26

Sec. 2.2: execution exploration.
Sec. 2.3: stateless search.
Sec. 3.1: region data structure and Fig. 4 symbolic reachability.

Lecture 4: April 27

Undecidability of reachability computation.
Bounded reachability and abstraction.
Predicate abstraction basics.

Tutorial 2: April 29

Partial orders, inference rules, sets and formulas

Lecture 5: May 3

- predicates, formulas defined by finite sets of predicates
- over-approximation, logical implication
- abstraction function for sets of states, abstract state
- predicate abstraction
- abstraction effieciency vs. precision, Cartesian abstraction
- abstract post function

Lecture 6: May 4

- algorithm ART: construction of abstract reachability trees
- antichains
- extention of ART with antichains
- expention of ART with counterexample construction
- feasible and spurious counterexamples, feasibiity checking
- basics of linear arithmetic, Farkas' lemma

Lecture 7: May 10

Additional material on interpolation PDF.
- Interpolation: motivation and definition
- Interpolation between disjoint convex hulls: definition and algorithm

Lecture 8: May 11

- potential counterexamples computed by ART
- check if counterecample is real or spurious
- characterization of desired abstraction refinement based on spurious counterexamples

Lecture 9: May 17

- connection between characterization of desired abstraction refinement and interpolation
- sequence of interpolants for spurious counterexample paths
- elimination of spurious counterexample through refined abstraction

Lecture 10: May 18

- proving non-reachability of the error location by induction
- induction hypothesis as safe inductive invariant
- encoding of invariant candidates through constraints
- simplification of constraints (existential and universal quantifiers) and their non-linearity

May 24 and 25: public holidays

Lecture 11: May 31

- Ranking function generation for a single loop (PDF)
- Well-founded relations
- Proving termination using multiple well-founded relations and transitive closure

Lecture 12: June 1

- abstraction and refinement for termination I

Lecture 13: June 2

- abstraction and refinement for termination II

Lecture 14: June 7

- formalization of programs with procedures

Lecture 15: June 8

- transitions in programs with procedures: operatinos, calls, returns
- transition relation over states with stack

Lecture 16: June 14

- inference rules as formalism for presenting algorithms
- summarization-based algorithm for concrete enumerative reachability for programs with procedures

Lecture 17: June 15

- formalization ofprograms with threads
- thread-modular concrete enumerative reachability for multi-threaded programs

Lecture 18: June 21

- Linear Time Logic (LTL) (see Part 3 on the slides courtesy of Stefan Schwoon)

Lecture 19: June 22

- Büchi automata (see Part 4 on the slides courtesy of Stefan Schwoon)

Lecture 20: June 28

- translation from LTL to (generalized) Büchi automata (see Part 5 on the slides courtesy of Stefan Schwoon)

Lecture 21: June 29

- verification of LTL properties using the automata-theoretic approach

Lecture 22: July 5

- lecture 21 continued

Lecture 23: July 6

- lecture 22 continued
- brief OCaml review

Lecture 24: July 12

- functional programming language, types, Hindley-Milner type inference

Lecture 25: July 13

- lecture 24 continued

Lecture 26: July 19

- refinement and liquid types for ML (see slides 1-62 by Ranjit Jhala)

Further references

An introduction to OCaml. See Part I
Programs as logical formulas and transition systems. See Sec 0.1, 0.2, and 0.3
Introduction to propositional logic. See Chapter 1 (public download) here.
Interpolation,invariant generation, and ranking functions for linear inequalities PDF.
How to write a proof by Tom Henzinger PDF.
A BBC4 documentary about understanding of infinity (YouTube video).