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.
Die Vorlesung beginnt am 10. Oktober. Wir empfehlen interessierten Studenten, die Keynote Vorträge der FMCAD Konferenz zu besuchen (am 3. und 4. Oktober jeweils um 9 Uhr im Kuppelsaal der TU Wien). Die Vorträge behandeln Anwendungen von Formaler Verifikation in der Industrie (Amazon und TTTech).
ECTS Breakdown: ECTS 6.0 = 150 Std.
Vorlesungseinheiten: 24 Std.
Vor- / Nachbereitung: 24 Std.
Implementierung der Übungsbeispiele: 3 x 33 Std.
Abgabegespräche: 3 Std.
Die Einfuehrungsvorlesung findet am 10. Oktober 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)
- 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.
