Trends and Pearls of Model Checking (Seminar)

Seminar in Theoretical CS, Winter Semester 2018/2019

News

  • 05.02.2019: The seminar talks will take place on Tuesday, February 12th, beginning at 9:00 in our seminar room (building E1, room 4201b).
  • 15.10.2018: We published the mapping from students to topics.
  • 10.10.2018: We made the introductory slides available.
  • 09.10.2018: Adapted number of seminar topics.
  • 25.09.2018: Published tentative datelines.
  • 11.07.2018: We are online.

Dates & Deadlines

Wed, 10.10.2018, 14:30 Kick-off meeting at seminar room of i2 (building E1, room 4201b)
Mon, 15.10.2018, 15:00 Topic preferences due
Tue, 16.10.2018 Topic notification
Mon, 29.10.2018 Detailed outline of report due
Mon, 19.11.2018 One chapter of report due
Mon, 10.12.2018 Full report due
Mon, 14.01.2019 Presentation slides due
Tue, 12.02.2019, 09:00 Seminar talks at seminar room of i2 (building E1, room 4201b)

Overview

Model checking is an automatic verification technique for both software and hardware systems. It systematically checks if a given model representing the system satisfies a property (e.g. a safety requirement) and therefore verifies if a system fulfills the desired behavior.

This seminar aims to give an overview of the research in the field of model checking. Each topic is covered by a scientific journal or conference article. These research articles are the basis on which students have to prepare their report and presentation. The presentations will be given at the end of the lecture period as a block seminar.

Prerequisites

Basic knowledge in the following areas is expected:

  • Formal languages and automata theory
  • Mathematical logic
  • Previous knowledge in model checking is helpful but not mandatory

Topics

Tools & Best Practices

  1. Literature 1: Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, Nir Piterman: T2: Temporal Property Verification. TACAS 2016: 387-393
    Literature 2: Byron Cook, Andreas Podelski, Andrey Rybalchenko: Proving program termination. Commun. ACM 54(5): 88-98 (2011)
    Supervisor: –
    Student: –
  2. Literature 1: K. Rustan M. Leino: Accessible Software Verification with Dafny. IEEE Software 34(6): 94-97 (2017)
    Literature 2: K. Rustan M. Leino: Dafny: An Automatic Program Verifier for Functional Correctness. LPAR (Dakar) 2010: 348-370
    Supervisor: –
    Student: –
  3. Literature: Cindy Eisner, Dana Fisman: Functional Specification of Hardware via Temporal Logic. Handbook of Model Checking 2018: 795-829
    Supervisor: –
    Student: –

Ideas in Modern Model Checking

  1. Property Directed Reachability via IC3. Literature to be announced.
    Supervisor: Sebastian Junges
    Student: Matteo Tschesche
  2. Literature: Ranjit Jhala, Andreas Podelski, Andrey Rybalchenko: Predicate Abstraction for Program Verification. Handbook of Model Checking 2018: 447-491
    Supervisor: Matthias Volk
    Student: Fynn Mazurkiewicz
  3. Literature: Kenneth L. McMillan: Interpolation and Model Checking. Handbook of Model Checking 2018: 421-446
    Supervisor: –
    Student: –
  4. Literature: Natarajan Shankar: Combining Model Checking and Deduction. Handbook of Model Checking 2018: 651-684
    Supervisor: Tim Quatmann
    Student: Ilja Alexandrov

Qualitative Model Checking Extensions

  1. Literature: Julian C. Bradfield, Igor Walukiewicz: The mu-calculus and Model Checking. Handbook of Model Checking 2018: 871-919
    Supervisor: –
    Student: –
  2. Literature: Rajeev Alur, Ahmed Bouajjani, Javier Esparza: Model Checking Procedural Programs. Handbook of Model Checking 2018: 541-572
    Supervisor: Sebastian Junges
    Student: Mengying Xue
  3.  

Model Checking Approaches for Concurrent Processes

  1. Literature: Aarti Gupta, Vineet Kahlon, Shaz Qadeer, Tayssir Touili: Model Checking Concurrent Programs. Handbook of Model Checking 2018: 573-611
    Supervisor: Sebastian Junges
    Student: Mietze Tang
  2. Literature: Parosh Aziz Abdulla, A. Prasad Sistla, Muralidhar Talupur: Model Checking Parameterized Systems. Handbook of Model Checking 2018: 685-725
    Supervisor: Sebastian Junges
    Student: Paul Lambrich
  3. Literature:  Dimitra Giannakopoulou, Kedar S. Namjoshi, Corina S. Păsăreanu: Compositional Reasoning. Handbook fo Model Checking 2018: 345-383
    Supervisor: Sebastian Junges
    Student: Dennis Ledwon

Additional Material

Registration

Registration to the seminar is organised via a central application procedure. Belated registrations are not possible..

Contact

Matthias Volk <matthias.volk at cs.rwth-aachen.de>