Module Description

Module: Model Checking - Proof Engines and Algorithms

Courses:

TitleTypeHrs/WeekPeriod
Model Checking - Proof Engines and AlgorithmsLecture2Summer Semester
Model Checking - Proof Engines and AlgorithmsRecitation Section (small)2Summer Semester

Module Responsibility:

Prof. Görschwin Fey

Admission Requirements:

None

Recommended Previous Knowledge:

Basic knowledge about data structures and algorithms

Educational Objectives:

Professional Competence

Theoretical Knowledge

Students know

  • algorithms and data structures for model checking,
  • basics of Boolean reasoning engines and
  • the impact of specification and modelling on the computational effort for model checking.
Capabilities

Students can

  • explain and implement algorithms and data structures for model checking,
  • decide whether a given problem can be solved using Boolean reasoning or model checking, and
  • implement the respective algorithms.

Personal Competence

Social Competence

Students

  • discuss relevant topics in class and
  • defend their solutions orally.
Autonomy

Using accompanying material students independently learn in-depth relations between concepts explained in the lecture and additional solution strategies.

ECTS-Credit Points Module:

6 ECTS

Examination:

Oral exam

Workload in Hours:

Independent Study Time: 124, Study Time in Lecture: 56


Course: Model Checking - Proof Engines and Algorithms

Lecturer:

Görschwin Fey

Language:

German & English

Period:

Summer Semester

Content:

Correctness is a major concern in embedded systems. Model checking can fully automatically proof formal properties about digital hardware or software. Such properties are given in temporal logic, e.g., to prove "No two orthogonal traffic lights will ever be green."

And how do the underlying reasoning algorithms work so effectively in practice despite a computational complexity of NP hardness and beyond?

But what are the limitations of model checking?
How are the models generated from a given design?
The lecture will answer these questions. Open source tools will be used to gather a practical experience.

Among other topics, the lecture will consider the following topics:

  • Modelling digital Hardware, Software, and Cyber Physical Systems

  • Data structures, decision procedures and proof engines

    • Binary Decision Diagrams

    • And-Inverter-Graphs

    • Boolean Satisfiability

    • Satisfiability Modulo Theories

  • Specification Languages

    • CTL

    • LTL

    • System Verilog Assertions

  • Algorithms for

    • Reachability Analysis

    • Symbolic CTL Checking

    • Bounded LTL-Model Checking

    • Optimizations, e.g., induction, abstraction

  • Quality assurance

Literature:

Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, MA, USA.

A. Biere, A. Biere, M. Heule, H. van Maaren, and T. Walsh. 2009. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam, The Netherlands, The Netherlands.

Selected research papers