Die Vorlesung beschäftigt sich mit der automatischen Verifizierung von Programmen. Der Fokus liegt hierbei auf den algorithmischen Aspekten der Verifikation. Die Vorlesung setzt sich aus zwei Teilen zusammen:
Im ersten Teil behandeln wir die Verifikation von Modellen mit einem endlichen Zustandsraum (z.B. manuell erstellte Abstraktionen, Zustandsdiagramme, Kontrollsoftware in eingebetteten Systemen).
Im zweiten Teil der Vorlesung erweitern wir diese Ansätze, um die Verifikation von parallelen Programmen und Programmen, deren Zustandsraum nicht a priori beschränkt ist, zu ermöglichen.
ECTS Breakdown: ECTS 6.0 = 150 Std.
Vorlesungseinheiten: 48 Std.
Vor- / Nachbereitung: 20 Std.
Implementierung der Übungsbeispiele: 4 x 20 Std.
Abgabegespräche: 2 Std.
Die Einfuehrungsvorlesung findet am 3. Maerz statt.
Inhalt der Vorlesungseinheiten:
The Basics
The first part of the course covers semantics and the encodig of transition functions.
- Introduction and motivation: Outline of the course, the necessity for automated verification (software desasters), success stories, and potention future applications
- One small step for a man: Small step semantics: Hoare logic and Dijkstra's predicate transformers, Kripke structures, encoding transition functions.
Part I
From single step transitions to bounded model checking, specifying reachability and temporal logic properties, and the computation of fixed points.
- Bounded Model Checking: Specifying and checking reachability/safety properties, unwinding transition functions, completeness conditions (reachability/recurrence diameter). Shows how BMC can be applied to check safety properties for software ("local" rather than "monolitic" transition functions). Discusses application for automated test-case generation.
- Decision Procedures: How do we decide the instances of formulas generated by BMC? Satisfiability (SAT) checking, Satisfiability-Modulo-Theory (SMT) solvers, Binary Decision Diagrams (BDDs)
- Back to the Future (Temporal Logic): Temporal logic, the flagship formalism of the model checking community. Linear Temporal Logic (LTL), Computation Tree Logic (CTL)
- Groundhog Day (Computing Fixed Points):Translating temporal logic formulas into fixed point a brief outline of the ¿-calculus. Efficient computation of fixed points: symbolic model checking
- Approximating Fixed Points (Craig Interpolation): Approximating Fixed Points with Craig Interpolation
- Partial Order Reduction (optional): Reducing the size of the state-space for concurrent models by means of partial order reduction (POR)
Part II: To infinity and beyond
Shows how the ideas presented in part I can be applied to infinite state systems (and actual software programs rather than models) by means of abstraction. Introduces static analysis using abstract interpretation, predicate abstraction, and interpolation-based software model checking. The course may cover advanced concepts such as rely/guarantee reasoning for parallel programs (Owicki-Gries) and temination proving, if time permits.
- the Concept of Abstraction (Abstract Interpretation): Static analysis of programs using abstraction and abstract domains. Disjunctive domains and loss of precision.
- Predicate Abstraction and Automated Refinement: Tracking facts about program states using first-order logic predicates.Automatically refining abstractions using Counterexample-Guided Abstraction-Refinement (CEGAR)
- Lazy Abstraction, Interpolation-based Software Model Checking: Contemporary techniques for predicate abstraction and automated refinement
- Concurrent Software Hoare logic for parallel programs with shared memory. Owicki-Gries, Cliff Jones' rely-guarantee reasoning (compositional reasoning). Automatic refinement of environment assumptions. Global vs. local invariants and ghost variables. Also addresses incomplete approaches such as context-bounded model checking.
- Provig Termination: Ranking functions. Automated construction of termination proofs based on Cook/Podelski/Rybalchenko's work.
Publikationen zu den Vorlesungseinheiten:
Hoare Logic
C.A.R. Hoare, "An axiomatic basis for computer programming", Communications of the ACM, 1969
Robert W. Floyd, "Assigning meanings to programs", Proceedings of the American Mathematical Society Symposia on Applied Mathematics, 1967
Greg Nelson, "A generalisation of Dijkstra's calculus", ACM Transactions on Programming Languages and Systems, 1989
Ten Years of Hoare's Logic: A Survey Part l. KRZYSZTOF R. APT
Bounded Model Checking
Edmund M. Clarke, Daniel Kroening, Flavio Lerda, "A Tool for Checking ANSI-C Programs", TACAS 2004
Satisfiability Checking
G. Weissenbacher, S. Malik, "Boolean Satisfiability Solvers: Techniques and Extensions", Software Safety and Security - Tools for Analysis and Verification, NATO Science for Peace and Security Series, IOS Press, 2012
D. Kroening, O. Strichman, "Decision Procedures - An Algorithmic Point of View", Springer 2008
