| Course | Exams | Lecture Notes | Problem Sets |
Verification
Core course (offered in block form after lecture period)
Summer term 2013 (September 2013. Receive updates on our mailing list.)
| People: | Bernd Finkbeiner, Martin Zimmermann, Peter Faymonville, Leander Tentrup |
| Lecture Room: | E1 3, HS001 |
| Lecture Period: | September 9th – October 9th |
| Office Hours: | Bernd Finkbeiner: Wednesdays 15:00-16:00 E 1 3 / 506 Martin Zimmermann: E 1 3 / 533 Peter Faymonville: E 1 3 / 533 Leander Tentrup: E 1 3 / 532 |
| Contact: | verification at react.uni-saarland.de |
News
- 15.10.2013: The re-exam results are updated.
- 10.10.2013: The re-exam inspection is on Tuesday, December 10th, at 12:01pm in building E1 3, room 528.
- 26.11.2013: The re-exam results are online.
- 05.11.2013: The backup exam is on Monday, November 25th, at 10am in building E1 3, HS 002. Please send a mail at verification at react.uni-saarland.de if you want to take part in the exam.
- 15.10.2013: The exam results are updated.
- 10.10.2013: The exam inspection is on Tuesday, October 15th, at 10am in building E1 3, room 528.
- 09.10.2013: The exam results are online.
- 05.10.2013: The exam is on Wednesday, October 9th, at 9am in building E2 2, “Günter-Hotz-Hörsaal”. The exam is open book! A list of students that are allowed to take part in the exam is online. If you have more than 50% of the points and you cannot find your student id in the list then send an email (including your student id) at verification at react.uni-saarland.de.
- 01.10.2013: There will be a review session at Monday, October 7th, at 2pm in E1 3, HS001.
- 26.09.2013: The backup exam will take place at November 25th, 2013.
- 13.09.2013: You can download the result of our evaluation .
- 09.09.2013: We have uploaded the group chart.
- 06.09.2013: On September 9th, we will have our first lecture of the block course at 9:00 am (s.t.) in lecture hall 1, building E1 3.
- 23.08.2013:
In case you have not already registered, please remember to register for this course in LSF in order to get a course certificate (Schein) at the end of the lecture.
There will be small practical exercises where you experiment with model-checking tools. Make sure you download, install and test the following tools:
- VIS
- SPIN
- Uppaal - 13.06.2013: Added information regarding course structure, exam regulations
- 15.04.2013: Subscribe to our mailing list to automatically receive updates.
- 12.04.2013: The lecture will be held as a block course after the lecture period. More information will be available during the semester.
- 25.03.2013: Lecture website online
Structure
This course is held in block form after the lecture period. Except for wednesdays, we’re going to meet every weekday for two sessions, a morning session (from 9:00am to 11:30am) and an afternoon session (from 2:00pm to 4:30pm). On wednesday there is only the morning session. Each session starts with a 60min lecture, followed by roughly an hour of group working time on the assignments. At the end of the session you’re going to discuss your groups’ solutions with your tutor. We’ll grade you on the performance in these meetings.
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