Instructors
- Lectures: Prof. Jan Kretinsky
- Tutorials: Kush Grover and Muqsit Azeem
Overview
- Module IN2050
- Lectures: Tuesdays 12:00-14:00 in 03.13.010, Seminarraum (5613.03.010) and Wednesdays 12:00 - 14:00 in 03.09.014, Seminarraum (5609.03.014) (starting on Apr 26).
- Tutorials: Mondays 16:00 - 18:00 (starting on May 02) in 03.13.010, Seminarraum (5613.03.010).
- Language: English
- Registration: Please register for both Lectures and Exercises
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.
Slides
Slides for the course prepared by Javier Esparza, Stefan Schwoon, and Jan Kretinsky:
Project: Bonus Exercise
Flash news! We are launching a new bonus exercise: Implement a Model Checker. You will get a chance to build your own little on-the-fly model checker in 6 weeks.