| Course | Tutorials | Exams | Lecture Notes | Problem Sets |
Verification
Core Lecture Course (9 CP)
Wintersemester 2011/2012
| People: | Bernd Finkbeiner, Peter Faymonville, Michael Gerke |
| Lecture Room: | HS 003 Building E 1 3 |
| Lecture Time: | Tuesdays 16:15-17:55 and Thursdays 14:15-15:55 |
| Tutorials: | Mondays 16:00-18:00 E 1 3 SR 015, Wednesdays 12:00-14:00 E 1 3 SR 015 |
| Office Hours: | Bernd Finkbeiner: Wednesdays 15:00-16:00 E 1 3 / 506 Peter Faymonville: E 1 3 / 533 Michael Gerke: E 1 3 / 507 |
News
- 20.3.2012 The results of the endterm exam are online available.
- 14.2.2012 The results of the final exam are online available.
- 31.1.2012 Twelfth Problem Set available
- 19.1.2012 Eleventh Problem Set available (πVC tool, πVC tutorial, Abs.pi, InsertionSort.pi)
- 13.1.2012 There is a new version of Problem Set 10 online. The return statement was missing from function abs.
- 12.1.2012 Tenth Problem Set available
- 3.1.2012 Exam Inspection will be held Wednesday next week (11th), 2pm – 4pm in room 528
- 3.1.2012 There will be no tutorials next week, only discussion slots
- 23.12.2011 Ninth Problem Set available
- 22.12.2011 The results of the midterm exam are online available.
Note: A grade of 4 or better means exam passed, 5 means not passed. - 22.12.2011: In our lecture today, we’ll talk about the verification of the FlexRay physical layer protocol (see Lecture Notes), which, by the way, was the topic of Michael’s Master thesis. For this work, Michael received the Young Scientist Award 2011 in the category Dynamic Intelligent Systems (Computer Science and Embedded Systems).
- 13.12.2011: Eighth Problem Set available
- 5.12.2011: Our Midterm Exam will take place on Dec 20th, 4pm-7pm, Günter-Hotz-Hörsaal (building E2 2, formerly called Audimo)
- 1.12.2011: Seventh Problem Set available
- 28.11.2011: Sixth Problem Set available
- 17.11.2011: Fifth Problem Set available
- 10.11.2011: Fourth Problem Set available
- 27.10.2011: Second Problem Set available
- 20.10.2011: First Problem Set available
- 14.10.2011: Exam rules, problem sets modus
- 13.10.2011: Exam dates fixed
- 19.9.2011: Lecture website online
Syllabus
How can one ensure that computer programs actually do what they are intended to do? Simply running a program repeatedly with various inputs is inadequate, because one cannot tell which inputs might cause the program to fail. It is possible to tailor a tester to test a given program, but present-day programs are so complex that they cannot be adequately checked through conventional testing, which can leave significant bugs undetected. Program verification uses mathematical and logical methods to prove that a program is correct. This approach was pioneered by, among others, Dijkstra, Floyd, Gries, Hoare, Lamport, Manna, Owicki and Pnueli. Today, we have powerful decision procedures that can, completely automatically, answer basic questions about the data types typically used by programmers. Model Checking is a “push-button” technology that can analyze finite-state abstractions of programs with as many as 1020 states. This course takes an up-to-date look at the theory and practice of program verification.
Main Textbooks
- Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, 2008
- Krystof R. Apt, Frank S. de Boer, Ernst-Rüdiger Olderog: Verification of Sequential and Concurrent Programs, 2009
- Aaron R. Bradley and Zohar Manna: The Calculus of Computation (online version available through Springer Link).
- Zohar Manna, Amir Pnueli: Temporal Verification of Reactive Systems, 1995
Recommended Reading
- Temporal Verification of Reactive Systems – Safety by Zohar Manna and Amir Pnueli, Springer Verlag, ISBN: 0387944591
- Temporal Verification of Reactive Systems – Progress by Zohar Manna and Amir Pnueli (draft chapters available online)
- Principles of Model Checking by Christel Baier and Joost-Pieter Katoen
- Model Checking by Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, MIT Press; ISBN: 0262032708