News

• 25.09.2018: The exam review for the second exam will take place this Wednesday, September 26th, from 11:00-12:00 in lecture hall AH VI. Please bring your BlueCard.
• 20.09.18: The second exam for Model Checking takes place this Friday, September 21st, at 14:00 in AH IV. You are allowed to bring your copy of the slides and the Principles of Model Checking book. No own notes are allowed.
• 05.09.2018: The correction of the first exam has been completed. Please find your result in the L2P. The review for the exam will take place on Friday, 07.09, in room 5056. To prevent long queues, we partitioned the group based on their matriculation number as shown below. Please bring your BlueCard.
  

  Matriculation number	Time
  < 345 000	09:15 to 10:15
  > 345 000	10:15 to 11:15

• 23.08.18: Fixed a path in the solution of task 3(b) of sheet 4.
• 21.08.18: We uploaded the solution for the old exam.
• 20.08.18: Fixed a minor typo in the solution of sheet 5.
• 02.08.18: We uploaded an old exam as preparation for the exam.
• 16.07.18: There will be a Q&A session on Thursday, 23.8., from 9:30 to 12:30 in AH IV. Please send us your questions before the question session via mail.
• 06.07.18: two typo’s in the slides of lecture 19 have been fixed
• 27.06.18: We updated the sample solution of exercise sheet 8 to account for two missing transitions in task 1(c).
• 12.06.18: We updated the seventh exercise sheet to fix a typo in task 4(b).
• 29.05.18: Since we have not given the formal GNBA to NBA transformation in the lecture, we included it on exercise sheet 5.
• 18.05.18: Due to an unfortunate oversight, we updated the fourth exercise sheet to repair task 1 (again). We apologize for any inconveniences.
• 16.05.18: The period for the exam registration ends this Friday, 18th May. Make sure to register before this deadline.
• 16.05.18: We updated the fourth exercise sheet to fix a typo in task 3.
• 14.05.18: We updated the fourth exercise sheet to repair task 1.
• 03.05.18: We updated the second exercise sheet to make task 1 more precise.
• 30.04.18: The poll revealed that there are too many clashes when changing the date of the first exam, so we will stick to the old date (31 August).
• 23.04.18: The first exercise sheet is online.
• 20.04.18: We opened a poll in L2P to determine whether we need to shift the date of the first exam. Please indicate until next Wednesday whether you are available in specific time slots.
• 16.04.18: Please register to the L2P room for the lecture via Campus Office. Not only will announcements reach you more quickly, but questions concerning the lectures and exercises can be posted in the L2P forum.
• 13.04.18: We changed the room for the exercise class to AH II.
• 27.03.18: Adapted the dates for the first lectures and added information about the exams.
• 02.03.18: We are online.

Schedule

Slides

Exercises

Exam

You are allowed to bring your copy of the slides and the Principles of Model Checking book. No own notes are allowed.

Motivation

In 2008, the ACM awarded the prestigious Turing Award – the Nobel Prize in Computer Science – to the pioneers of Model Checking: Ed Clarke, Allen Emerson, and Joseph Sifakis.
  

Why?
Because model checking has evolved in the last twenty-five years into a widely used verification and debugging technique for both software and hardware.

It is used (and further developed) by companies and institutes such as IBM, Intel, NASA, Cadence, Microsoft, and Siemens, to mention a few, and has culminated in a series of mostly freely downloadable software tools that allow the automated verification of, for instance, C#-programs or combinational hardware circuits.

Subtle errors, for instance due to multi-threading, that remain undiscovered using simulation or peer reviewing can potentially be revealed using model checking.  Model checking is thus an effective technique to expose potential design errors and improve software and hardware reliability.

But how does it work, that is, what are its underlying principles?
That’s exactly the focus of this lecture series!

We will show that model checking is based on well-known paradigms from automata theory, graph algorithms, logic, and data structures.  Its complexity is analyzed using standard techniques from complexity theory.

Contents of the Lecture

Model checking is based on, well, checking models. So, we first start by explaining what models are, and will make clear that so-called labeled transition systems, a model that is akin to automata, are suitable for modeling sequential, as well as multi-threading programs.

This is followed by a detailed study on various classes of system properties such as safety, liveness, and fairness.  It will be shown how finite automata as well as variants thereof that accept infinite words are suitable for verifying regular properties.

The linear-time and branching time temporal logics LTL and CTL are then introduced and compared. Model checking algorithms for these logics together with detailed complexity considerations are covered.

Finally, abstraction techniques based on bisimulation and simulation relations are covered. These techniques are at key techniques to combat the state explosion problem.

Prerequisites

We expect students to have some basic knowledge in:

• Automata Theory
• Mathematical Logic
• Discrete Mathematics
• Complexity Theory
• Algorithms and Data Structures

The course book (see below) will contain a summary of the issues in these areas that are relevant to this lecture series.  We believe that this course is also well-suited for students in electrical engineeering and mathematics.

Materials

The course will basically cover Chapters 1 through 7 (upto section 7.3).

Additional literature:

• E.M. Clarke, O. Grumberg, D.A. Peled: Model Checking, MIT Press, 1999

• M. Huth and M.D. Ryan: Logic in Computer Science – Modelling and Reasoning about Systems, Cambridge University Press, 2nd edition, 2004

• K. Schneider: Verification of Reactive Systems, Springer-Verlag, Texts in Theoretical Computer Science. An EATCS Series, 2004