Schedule
Type
Day
Time
Place
Start
Lecturer
News
- Here are the results of the second exam. The exams may be inspected on Tuesday, 25.03 from 10:00 - 11:00 in our seminar room 4201b. Please do not forget to bring your student ID.
- The second exam will take place in AH 5 from 14:00 - 16:00.
- Here are the updated results of the first exam after the inspection. These results are now transferred to the ZPA. Due to a mistake in our own solution we have re-corrected question 5 for all students. All students that received points according to the faulty version have kept their points and students that spotted the mistake and solved the task correctly now also got points so in total the mark either stayed the same or got better for everyone but not worse. (25.02.2014)
- Here are the results of the first exam. The exams may be inspected on Monday, 24.04 from 11:00 - 12:00 in our seminar room 4201b. Please do not forget to bring your student ID.
- As a reminder for those who have not attended the exercise classes: the exam starts at 11:00! (not at 9:45 as campus office might suggest)
- First exam's room assignment: 218474 - 310601 in AH 4 and 310653 - 341454 in AH 5. (07.02.14)
- Please check the list of admitted students at the bottom of the page! If your matriculation number does not appear there but you have registered with ZPA and achieved at least 52 exercise points in total, please contact us as soon as possible! (07.02.14)
- Here is another old exam that you can use for practicing. (05.02.14)
- To answer a frequently asked question: in the exam the following material is explicitly allowed
- the book "Principles of Model Checking",
- a printout of the lecture slides,
- a dictionary.
- The lectures have ended, however there are 3 more exercise classes ahead: Wed 29.01.14 (discussion of series 12), Wed 05.02.14 (discussion of series 13) and Mon 10.02.14 (discussion of sample exam). The last class is absolutely optional but it is a good opportunity to see the solution of an exam and ask questions. It will take place in AH 6, 13:15 - 14:45.
- The overview of the points below has now beep updated and includes series 11. All mistakes that were pointed out to us should now be corrected. Please check. (27.01.14)
- Here is a sample exam that may help you with your preparations. Try to solve it in 120 minutes! We will discuss its solution in the last exercise class. (27.01.14)
- Below you find the current percentage of achieved points (that is up to and including series 9). We plan to have a total of 13 exercise sheets. (15.01.2014)
- Series 10 has been uploaded now. Note that these are regular exercise questions and might take more time (exercise 1 in particular) than the shorter exam questions which we discussed today. Don't panic! (08.01.2014)
- The Christmas series (series 9) is now online (19.12.2013)
- On Wednesday (18.12.2013) you will have the opportunity to evaluate the exercise class and give us some feedback!
- Remark for today's lecture: My explanation of the third example, slide 272 seemed to be not convincing for everybody. So let me explain it here again carefully: The fairness assumption only excludes one path, namely the one where the system cycles around "a" states forever. Thus every fair execution visits "b" states again and again with arbitrary many "a" states in between. Thus the following execution is fair "a b a a a b a ..." However it violates the given property. Once the "b" state is visited, the "Box (b iff Next a)" part of the until formula must hold. It means that the remaining execution "b a a a b a ..." satisfies that always there is a "b" if and only if the next label is an "a". This is violated by the two "a"s that follow one another. (02.12.2013)
- Today two students were still looking for an exercise partner. Everyone who still needs a partner please meet right after Monday's lecture in AH4. (27.11.2013)
- Remark regarding exercise series 4: none of the proof tasks require more than 4 lines of argument. Make sure you are precise and use definitions and facts from the lecture but if your argument requires half a page you probably doing things way too complicated. (14.11.2013)
- A corrected version of sheet 3 was uploaded (cf. task 1g). (07.11.2013, 11:46)
- There will be no lecture on Tue, 05.11.2013 due to the student union convention (Fachschaftsvollversammlung).
- The first exercise series will be uploaded tomorrow (Wed, 23.10). Please work in groups of two! You have one week to hand it in using the box at our chair or at the latest right BEFORE the exercise class starts (in AH6). Electronic solutions are not accepted.
- The first exercise class will be on October 30 (instead of October 23).
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.
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 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
This course is suitable for Hauptdiplom, bachelor (this course is part of the "Wahlkatalog" in theoretical computer science), as well as master students.
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.
Follow-up courses
This course provides the basis for the follow-up courses:
Advanced Model Checking
Model Checking Labs
Moreover, it is related to courses such as:
Advanced Model Checking
Model Checking Labs
Moreover, it is related to courses such as:
- Semantics and Verification of Software
- Automata and Reactive Systems (i7)
- Automata on Infinite Words (i7)
- Formal Methods for Embedded Systems (i11)
There are thus plenty of opportunities to combine this course with others! We also regularly offer seminars that are based on model checking and offer various master and diplom theses on model checking and its applications.
Slides and exercise sheets
Date | Lecture | Subject | Slides | Exercises | Solution |
|---|---|---|---|---|---|
Oct 14 | 1 | Motivation, Background, and Course Organization | |||
Oct 21 | 2 | Modeling Parallel Systems | |||
Oct 22 | 3 | Parallelism and Communication | |||
Oct 28 | 4 | Channel Systems | |||
Oct 29 | 5 | Linear Time Properties | |||
Nov 04 | 6 | Invariants and Safety | |||
Nov 11 | 7 | Liveness and Fairness | |||
Nov 12 | 8 | Regular Properties | |||
Nov 18 | 9 | Omega-regular Properties | |||
Nov 19 | 10 | B?chi Automata | cf. lec 9 | ||
Nov 25 | 11 | Model Checking with B?chi Automata | |||
Nov 26 | 12 | Linear Temporal Logic | |||
Dec 02 | 13 | LTL - continued | cf. lec 12 | ||
Dec 10 | 14 | LTL model checking | |||
Dec 16 | 15 | ... continued | cf. lec 14 | ||
Dec 17 | 16 | Complexity of LTL model checking | |||
Jan 06 | 17 | Computation Tree Logic | |||
Jan 07 | 18 | LTL versus CTL | |||
Jan 13 | 19 | CTL Model Checking | |||
Jan 20 | 20 | CTL Model Checking with fairness | |||
Jan 21 | 21 | CTL* and CTL+ | |||
Jan 27 | 22 | Bisimulation | |||
Admitted to first exam
218474
258010
263631
266638
269456
275526
275718
279082
279970
280162
283043
286205
287193
288144
290664
291717
293578
294875
296002
297686
300069
300760
302276
302289
302529
302559
303830
304074
304932
305100
305380
305436
305718
307752
308621
308641
308678
308704
308769
308811
308884
308888
309700
310057
310271
310279
310601
310653
310733
310747
311057
311256
311673
311733
312308
312501
312654
312666
312690
312696
312870
313186
313430
314391
314703
314923
314963
315250
316231
319462
319463
320667
321850
327824
327826
327907
336068
336970
340890
340892
340933
341023
341051
341052
341123
341127
341409
341454
Materials
The lectures and all materials are in english. The slides will be made available via this webpage during the course.
The course is based on the recently published book:
An errata document to the book may be found here.
It is possible to buy a book (about 40 euros), but there is no need to do so as there are various copies of the book available at the CS library.
- 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