Instructors

• Lectures: Prof. Jan Kretinsky
• Tutorials: Alexandros Evangelidis and Kush Grover

Overview

• Module IN2050
• Lectures: Tuesdays and Wednesdays 10:00 - 11:30 online (starting on Apr 13)
• Tutorials: Mondays 14:00 - 15:30 online  (starting on Apr 19)
• Language: English

Note that it is not necessary to have taken the course "Automata and Formal Languages" for enrolling on this course.

Content

Model-Checking is a technique for automatic verification of hardware and software systems. Given a system and a correctness specification, a model checker checks if the system works correctly.

Model Checking was invented in the mid 80s, and has made enormous progress, especially in the hardware sector. Nowadays all major hardware manufacturers have Model-Checking groups which have developed software tools for the verification of large circuits. In 2008, the inventors of Model Checking received the Turing-Award.

The course introduces the basics of Model Checking. It starts by showing how to model systems, and how to express correctness specifications using temporal logic. It then describes algorithms that automatically decide whether the model satisfies the properties. The course also presents some of the most popular academic Model-Checking tools, like Spin and NuSMV.

The only prerequisites for the course are basic notions of logic, graph theory, and algorithms.

News

• Retake exam, oral over bbb, to take place on the 12th of October. Precise timing information will be given later.
• Online forum for discussions and questions related to Model Checking 
• July 12: Exercise sheet 12 is available now.
• July 5: Exercise sheet 10 is available now.
• June 14: Exercise sheet 8 is available now.
• Changes in the schedule for upcoming weeks:
  31.05.2021, 14:00 - Lecture
  02.06.2021, 10:00 - Tutorial 6
  07.06.2021, 14:00 - Lecture
  09.06.2021, 10:00 - Tutorial 7
  14.06.2021, 14:00 - Lecture
  15.06.2021, 10:00 - Tutorial 8
• May 19: Exercise sheet 6 and updated Exercise sheet 5 is available now.
• May 13: Exercise sheet 5 is available now.
• May 5: Exercise sheet 4 is available now.
• Apr 7: Created webpage.

Slides

Slides for the course prepared by Javier Esparza, Stefan Schwoon, and Jan Kretinsky:

• PDF-File

 

External Links

The following tools are used in the lectures and in the exercises.

• Spin
• NuSMV
• DDcal can be downloaded from the web page of Fabio Somenzi.

  Follow the instructions in INSTALL to build the package.

      If you have a problem when installing the default version of perl/Tk from CPAN, download the lastest version Tk-804.033 and install it manually.

• Moped

  To quickly get started using Moped, you might want to use Docker with this pre-compiled image.

Here you can find specification patterns in LTL and other formalisms.