Course | Tutorials | Exams | Lecture Notes | Problem Sets |

# Verification

People: | Bernd Finkbeiner, Klaus Dräger, Andrey Kupriyanov, Michael Gerke |

Lecture Room: | HS 002 Building E 1 3 |

Lecture Time: | Tuesdays and Thursdays 14:15-15:55 |

Tutorials: | Room 014 Building E 1 3, Wednesdays 16:15-17:45 HS IV Math building E 2 4, Fridays 12:15-13:45 |

Office Hours: | Bernd Finkbeiner: Wednesdays 15:00-16:00 E 1 3 / 506 Klaus Dräger & Andrey Kupriyanov E 1 3 / 508 Michael Gerke E 1 3 / 507 |

## News

- Apr 19, 2010: The updated final grades after the final exam inspection are now available online
- Apr 12, 2010: The final exam inspection will take place on Thursday, April 15, at 14:00, in room 528, building E 1 3
- Apr 9, 2010: Final exam results and final grades are now available online
- Apr 6, 2010: The final exam will take place on Thursday, April 8, at
**2:30pm**(please come 5 minutes earlier), in HS 002, building E 1 3 - Feb 9, 2010: The endterm exam inspection will take place on Tuesday, February 16, at 14:00, in room 528, building E 1 3
- Feb 8, 2010: Endterm results are now available online
- Feb 1, 2010: Example solutions for the 9th, 10th and 11th problem sets are now available
- Feb 1, 2010: Intermediate list of course participants admitted to the final exam by 01.02.2010 is now available online
- Jan 29, 2010: The endterm exam will take place on Friday, January 5, at
**2:30pm**(please come 5 minutes earlier), in HS 002, building E 1 3 - Jan 15, 2010: Some features have been added to the LTL-part of the framework, please download the updated version
- Jan 14, 2010: All the lectures from now on will take place in room 407, building E 1 1
- Jan 14, 2010: Small error fixed in the framework, please download the updated version
- Jan 07, 2010: Framework for the practical project is now available online
- Jan 07, 2010: Next lecture on January 12 will take place in room 407, building E 1 1
- Dec 21, 2009: Midterm results are now available online
- Dec 16, 2009: Example solution for the 8th problem set is now available
- Dec 14, 2009: Example solution for the 7th problem set is now available
- Dec 11, 2009: Example solution for the 6th problem set is now available
- Dec 8, 2009: Example solutions for the 4th and 5th problem sets are now available
- Nov 19, 2009: Deadline for HISPOS registration: Dec 3, 2009
- Nov 18, 2009: Example solutions for the second and third problem sets are now available
- Nov 12, 2009: An example solution for the first problem set is now available
- Nov 6, 2009: A new version of the lecture from Oct 22, 2009 is available (fixed a typo)

## 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 10^{20} 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
- 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 (available in Spring 2008; selected chapters will be distributed in class)
- Model Checking by Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, MIT Press; ISBN: 0262032708