192.106 Software Model Checking
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2020W, VU, 4.0h, 6.0EC
TUWEL

Properties

  • Semester hours: 4.0
  • Credits: 6.0
  • Type: VU Lecture and Exercise
  • Format: Distance Learning

Learning outcomes

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.

Subject of course

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.

Teaching methods

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.

Mode of examination

Oral

Additional information

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

Lecturers

Institute

Course dates

DayTimeDateLocationDescription
Tue15:00 - 17:0006.10.2020 - 15.12.2020 See lecture announcement and slides "Introduction", page 35 (LIVE)Software Model Checking Lecture
Fri14:00 - 16:0009.10.2020 - 18.12.2020 See lecture announcement and slides "Introduction", page 35 (LIVE)Software Model Checking Lecture
Software Model Checking - Single appointments
DayDateTimeLocationDescription
Tue06.10.202015:00 - 17:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Fri09.10.202014:00 - 16:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Tue13.10.202015:00 - 17:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Fri16.10.202014:00 - 16:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Tue20.10.202015:00 - 17:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Fri23.10.202014:00 - 16:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Tue27.10.202015:00 - 17:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Fri30.10.202014:00 - 16:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Tue03.11.202015:00 - 17:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Fri06.11.202014:00 - 16:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Tue10.11.202015:00 - 17:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Fri13.11.202014:00 - 16:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Tue17.11.202015:00 - 17:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Fri20.11.202014:00 - 16:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Tue24.11.202015:00 - 17:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Fri27.11.202014:00 - 16:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Tue01.12.202015:00 - 17:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Fri04.12.202014:00 - 16:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Fri11.12.202014:00 - 16:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture
Tue15.12.202015:00 - 17:00 See lecture announcement and slides "Introduction", page 35Software Model Checking Lecture

Examination modalities

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.

Course registration

Begin End Deregistration end
30.09.2020 00:01 30.10.2020 23:59 31.12.2020 23:59

Curricula

Literature

No lecture notes are available.

Previous knowledge

Familiarity with propositional logic and first order logic.

Language

English