Lab Course Verification

Bernd Finkbeiner, Room 506, Building E 1 3, office hours Wednesdays 15-16

Tom In der Rieden

Syllabus

In this lab course we apply computer-aided verification tools to obtain a mathematical proof that an entire computer system is correct. Our target application is a simple communication tool, which we analyze across all system layers, including the hardware and the operating system. For this task we apply a range of verification tools, like computer-aided theorem provers (ISABELLE) and model checkers (SMV, SPIN).

The course consists of daily lectures and exercises in small groups over two weeks (Oct 4 – Oct 14, 2005). Grading will be based on a project presentation after the course. There are no strict prerequisites for this course; however, previous exposure to logic, verification, and/or computer architecture is helpful.