Document Actions
Model Checking (Vorlesung)
Model checking is a technique for the automatic verification of hardware or software systems. Given such a system and a specification of its intended behaviour, a model checker finds out whether the system satisfies the specification. Model checking has made enormous progress since its invention in the 1980s; today it is possible to verify entire CPU designs, and so all major microprocessor companies use and develop tools for this purpose. Software verification is more challenging and an active research topic (pursued at the chair for Software Engineering, for instance!). Recent years have seen interesting progress in this area as well. The course provides an introduction to the topic, covering how to model systems, how to express properties about them in temporal logic, and algorithms for checking whether they hold. We will introduce some well-known model-checking tools such as Spin and SMV.
Announcements:
- General information about SPIN can be found here. SPIN can be downloaded from here. Shell script which may help you to work with SPIN can be downloaded here.
- The first exercise group will take place on the 29th of April at 11 a.m. in the room SR 00-034, Geb. 051.
Slides:
- Final version of the slides
- Slides on timed automata (by Javier Esparza, see slides 23-72 - not relevant for the exam)
Exercise sheets:
- Instructors: Stefan Schwoon
- Times & Locations: Di 11-13 SR 00-034, Geb. 051 | Mi 11-13 SR 00-034, Geb. 051 - every other week
- Tutors: Sergiy Bogomolov
- Times & Locations of tutorials: Mi 11-13 SR 00-034, Geb. 051 - every other week