Software Model Checking

Advanced course in Winter 2007/08. 6 CP.

Instructor: Andrey Rybalchenko

Lectures: Monday, 10:00-12:00 in E1 4 (MPI building), room 024.

Tutorials: 2 hours per week. Thursdays, 12:00-14:00. E1 4 (MPI building), 6th floor, rotunda.

Final exam: Monday, 9:00. February, 18th, 2008.

Materials: Project assigments:
  1. DART algorithm. From AST to CFG.
  2. Invariants. Symbolic Execution. We shall have a preliminary discussion on it during November 29-tutorial.

Course description: Software systems are the most complex artifact that are built routinely, and are very difficult to get right. Automatic verification is indispensable to manage the continually increasing complexity of software systems.

We shall study software verification tools that employ logical reasoning about program computations, their abstraction, and abstraction refinement. We will learn principles, methods and algorithms that help building a state-of-the-art software verification tool. We will practically apply the knowledge from the classroom to develop such a tool.

Topics: Projects: we shall experiment with implementations of basic algorithms and shall build a state-of-the-art software model checker by the end of the class.

Prerequisites: basic knowledge in theoretical computer science. Background in verification, logics, and program analysis is useful, but not mandatory.

Grading: Grades will be awarded on the basis of homework assignments (30 %), paper presentation (10 %), and a final exam (60 %).