There's a strong focus on  practical aspects: the students will get the opportunity to work with widely used model checking tools such as CBMC of SMV, but will also implement their own model checker or extend an existing tool.

This course covers contemporary automated verification techniques for software. The focus is on the underlying techniques and algorithms rather than on using verfication tools. The course is divided into two main parts:

One covering model checking for finte state models (e.g., manual abstractions or UML state-charts), and a second part that shows how these techniques can be applied to actual implementations (i.e., infinite state programs) by means of abstraction.

ECTS Breakdown: ECTS 6.0 = 150 Std.

Lectures: 48 hours.

Preparation: 20 hours.

Implementing practical exercises: 4 x 20 hours.

Discussion of exercises: 2 hours

The introductory lecture takes place on March 3.

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.

Students are expected to read the research papers (typically 15-20 pages per week) listed on the course website before class.

The practical part consists of 3-4 short assignments and one research project, which will be split up into several incremental tasks.

Grading is based on class participation and project work.

Slides and links to papers covering the presented material will be provided, there is no need to buy books.

Entrace exam (March 10, 2015), topic: first-order logic and programming.

Papers about the lecture content:

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

This course has been postponed to 2016W and will not be held in 2016S.