Welcome to Verification!
We have two small corrections regarding dates and times: First, we had to move the time slot for our office hour. The office hour will take place Mondays, 1pm - 3pm (not 2pm - 4pm). Second, other than written on the... Read more
Welcome to Verification!
We have two small corrections regarding dates and times: First, we had to move the time slot for our office hour. The office hour will take place Mondays, 1pm - 3pm (not 2pm - 4pm). Second, other than written on the slides today, the first assignment will be handed out next Tuesday after the lecture. It is due Tuesday the week after, before the lecture starts. The slides will be updated accordingly.
Looking forward to the coming semester,
Your Verification Team
Core Lecture Course (9 CP)
Lectures: Tuesday 2-4 pm and Thursday 10-12 am in HS001, E1.3.
Tutorials: Wednesday 10-12 am or 2-4 pm in E1.1, Room 1.06.
Office Hours: Monday 1-3pm in E1.1, Room 1.06
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.
- Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, 2008
- Aaron R. Bradley and Zohar Manna: The Calculus of Computation (online version available through Springer Link).
- Temporal Verification of Reactive Systems – Safety by Zohar Manna and Amir Pnueli, Springer Verlag, ISBN: 0387944591
- Model Checking by Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, MIT Press; ISBN: 0262032708
- Krystof R. Apt, Frank S. de Boer, Ernst-Rüdiger Olderog: Verification of Sequential and Concurrent Programs, 2009