184.747 Software Model Checking Abgesagt
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2016S, VU, 4.0h, 6.0EC

Merkmale

  • Semesterwochenstunden: 4.0
  • ECTS: 6.0
  • Typ: VU Vorlesung mit Übung

Ziele der Lehrveranstaltung

Im Rahmen der Vorlesung werden die Studenten den praktischen Umgang mit existierenden Verifikationstools (so wie CBMC) erlernen und einen eigenen Model Checker entwickeln.

Inhalt der Lehrveranstaltung

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.

Weitere Informationen

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.

Vortragende Personen

Institut

Leistungsnachweis

Es wird von den Studenten erwartet, sich auf die Vorlesung vorzubereiten und die relevanten Publikationen zu lesen.

Die Note ergibt sich aus der Note für ein praktisches Projekt, das von den Studenten implementiert wird, und aus der Mitarbeit während der Vorlesung.

LVA-Anmeldung

Von Bis Abmeldung bis
01.03.2016 12:00 26.04.2016 23:59 27.05.2016 23:59

Anmeldemodalitäten

Positiver Eingangstest (10. Maerz 2015) zum Thema Praedikatenlogik und Programmierung

Curricula

Literatur

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


Vorkenntnisse

Diese Vorlesung wurde auf das Wintersemester 2016 verschoben und wird im Sommersemester 2016 nicht abgehalten.

Sprache

Englisch