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 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
- 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