Verification

People:	Bernd Finkbeiner, Sven Schewe, Rayna Dimitrova, Lars Kuhtz, Anne Proetzsch
Lecture Room:	HS 002 Building E 1 3
Lecture Time:	Tuesdays and Thursdays 14:15-15:45
Tutorials:	Room 013 Building E 1 3, Wednesdays 14:15-15:45 Room 013 Building E 1 3, Fridays 10:00-11:30
Office Hours:	Wednesdays 14:00-15:00

News

Apr 14, 2008: Backup exam grades and course grades are available online (password required)
Exam inspection will be on Friday, April 18, 2008, from 2pm to 4pm (Date changed!).
Feb 25, 2008: Final exam grades and course grades are available online (password required) Exam inspection will be on Monday, March 10, 2008, from 3pm to 5pm.
Feb 19, 2008: Reminder: The final exam is this Friday, 22.02.2008, 4:00pm – 6:00pm in HS 002 Building E1 3. See also the exams page. As we discussed, the relevant material for the final exam and the backup exam includes Lectures 1 through 26 (i.e., the entire course except for the last lecture on abstraction), including parts that appeared in the midterm and parts that were not covered in the tutorial.
Feb 17, 2008: There will be no tutorial in the week of Feb 20/22. The last lecture will be on Tuesday, Feb 19. We will be available for questions etc., however, during the usual tutorial and lecture times on Wednesday and Thursday (come see us on the 5th floor).
Feb 13, 2008: The list of students admitted to the exam is available online (password required).
Jan 6, 2008: Only two days left for the course evaluation via CLIX. The evaluation form is activated from January 28 — February 08, 2008. General information about course evaluations and CLIX is avaliable here.
Jan 3, 2008: Midterm grades are available online (password required) Exam inspection will be on Monday, January 21, 2008, from 3pm to 5pm. The midterm exam (password required).
Jan 3, 2008: There will be no tutorial in the week of Jan 9/11. Tutorials will start again on January 16.
Dec 13, 2007: In preparation for the midterm on Thursday, Dec 20, we will have a tutorial instead of the lecture on Tuesday, Dec 18. (There will be no tutorial on Wednesday or Friday.) For details about the midterm please check the exams page.
Nov 23, 2007: New version of problem set 4. Fixes a typo in the mutex property in problem 1.
Nov 16, 2007: For problem set 3, we provide a template file for problem 2 of problem set 3.
Nov 2, 2007: Deadline for HISPOS registration: 01.12.2007

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.

Verification

News

Syllabus

Recommended Reading