After successful completion of the course, students are able to use and implement software model checking tools. Successful participants are familiar with the state-of-the art algorithms in software model checking. They can apply software model checking tools in simple projects and estimate the required effort and benefit of deploying software model checking in larger projects. Moreover, the students will be able to implement a basic model checking tool.

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.

This course conveys the contents by means of classroom lectures given by the lecturer. Students are expected to read recent scientific publications on the topic as preparation for the course. Moreover, the theoretical content will be accompagnied by practical exercises, including the use of state-of-the-art verification tools as well as the implementation of a simple model checking tool.

This course is taught in English and held online.

Zoom Meetings Tuesday:

Meeting ID: 954 1816 7847
Password: SoMoCh20

https://tuwien.zoom.us/j/95418167847?pwd=eTZ1aEE4R3dOQ2Z5VFZIaU9xem1mdz09

Zoom Meetings Friday:

Meeting ID: 983 6354 2656
Password: SoMoCh20

https://tuwien.zoom.us/j/98363542656?pwd=VDRKZEk3enZzTlVCNkxNYUJ4eWh0Zz09

The grade is determined by the grade for the practical part (implementation of a model checker and a code walkthrough) and the grade of an oral exam (questions about the theoretical content of the course, as part of the code walkthrough). Both parts are weighted equally.

Familiarity with propositional logic and first order logic.