Model-Checking SS 2013

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

Lecture 1 (15.04.2013)

• Propositional logic: syntax, semantics, satisfaction relation

Lecture 2 (16.04.2013)

• Linear arithmetic: syntax, semantics, satisfaction relation
• Interpreted and uninterpreted predicates in the theory of linear arithmetic
• Clauses: syntax, semantics, satisfaction relation
• pic 1, pic 2, pic 3, pic 4

Lecture 3 (22.04.2013)

• Inference algorithms for Horn clauses, bounded unfoldings: explicit reasoning, symbolic reasoning
• pic 1, pic 2, pic 3

Lecture 4 (23.04.2013)

• Inference algorithms for Horn clauses: unbounded unfoldings, abstract inference
• pic 1, pic 2, pic 3, pic 4

Lecture 5 (29.04.2013)

• Programs as transition systems
• Correctness properties: safety, termination
• pic 1, pic 2, pic 3, pic 4

Lecture 6 (30.04.2013)

• Safety proof rule as Horn clauses: soundness, completeness
• Termination proof rule
• pic 1, pic 2, pic 3

Notes from the first six lectures (pdf).

Lecture 7 (6.05.2013)

• Predicate abstraction, apply abstract inference algorithm
• Termination arguments
• pic 1, pic 2, pic 3

Lecture 8 (7.05.2013)

• Procedural programs as transition systems
• Reachable states for procedural programs
• pic 1, pic 2, pic 3, pic 4

Lectures 7 and 8 added in the notes here (pdf).

Lecture 9 (13.05.2013)

• Summarization proof rule for procedural programs
• Multi-threaded programs as transition systems
• Reachable states for multi-threaded programs
• pic 1, pic 2, pic 3, pic 4

Lecture 10 (27.05.2013)

• Abstraction refinement as solving recursion-free Horn clauses
• Solving recursion-free Horn clauses using the Farkas lemma
• pic 1, pic 2, pic 3, pic 4, pic 5

Lecture 11 (28.05.2013)

• Solving recursion-free Horn clauses using the Farkas lemma (continued)
• pic 1, pic 2, pic 3, pic 4, pic 5

Lecture 12 (03.06.2013)

• Full algorithm for solving recursive Horn clauses using abstraction and refinement 1
• pic 1, pic 2, pic 3, pic 4

Lecture 13 (04.06.2013)

• Full algorithm for solving recursive Horn clauses using abstraction and refinement 2
• pic 1, pic 2, pic 3, pic 4

Lecture 14 (10.06.2013)

• Functional programs: definition, typing with base types (PDF)
• pic 1, pic 2, pic 3, pic 4

Lecture 15 (11.06.2013)

• Guest lecture by Klaus v. Gleissenthal on Barvinok's algorithm

Lecture 16 (17.06.2013)

• Functional programs: refinement types (PDF)
• pic 1, pic 2, pic 3, pic 4

Lecture 16 (17.06.2013)

• Functional programs: refinement types 2 (PDF)
• Linear Temporal Logic: syntax, semantics, stating the model checking problem
• pic 1, pic 2, pic 3, pic 4

Lecture 17 (24.06.2013)

• LTL to Buechi Automata, synchronous product of monitor x program
• pic 1, pic 2, pic 3

Lecture 18 (25.06.2013)

• Proof rule for fair termination
• pic 1, pic 2, pic 3