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 (Programming experience in C or C-like languages is required!).

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.

The course starts on 10th of October. Before that, we recommend that interested students attend the invited talks of the FMCAD conference (http://fmcad.org/FMCAD17/program) on October 3, 9am and October 4, 9am, on the use of automated verification techniques in industry (Amazon and TTTech). The keynotes are held in the Kuppelsaal of TU Wien.

ECTS Breakdown: ECTS 6.0 = 150 Std.

Lectures: 24 hours.

Preparation: 24 hours.

Implementing practical exercises: 3 x 33 hours.

Discussion of exercises: 3 hours

The introductory lecture takes place on October 10.

Course content:

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.

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.

Vizel et al.: Boolean Satisfiability Solvers and Their Applications in Model Checking
Proceedings of the IEEE, Volume: 103 Issue: 11, 2015

D'Silva et al.: A Survey of Automated Techniques for Formal Software Verification
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Volume 27, Issue 7, 2008