Software Model Checking

Advanced course in Winter 2007/08. 6 CP.

Instructor: Andrey Rybalchenko

News:

(Jan 12) No class on Jan 13 (POPL)
(Nov 29) Third project assignment due on December 3rd, 2007.
(Nov 29) Abstract interpretation and Galois connection: Sec 1-4.
(Nov 27) Notes for the 5th lecture online.
(Nov 20) Second project assignment due on November 26th, 2007.
(Nov 20) Sample Prolog code.
(Nov 8) Finalizing project account setup.
(Nov 8) First project assignment due on November 12th and 15th.
(Nov 5) Notes for the 2nd lecture online.
(Nov 4) Deadline for HISPOS registration: December 1st, 2007.
(Oct 29) For project account, please send me ASAP:
- your first/last name, email address, student id, desired account name.
(Oct 29) Tutorials:
- Time: Thursdays, 12:00-14:00. No tutorial on November 1st (holiday).
- Place: E1 4 (MPI building), 6th floor, rotunda.

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:

1st lecture, October 29. PPT
2nd lecture, November 5. PPT, PDF
4th lecture, November 19. PDF
5th lecture, November 26. PDF
6th lecture, December 03. Foundations and applications. RD, AE, LV
7th lecture, December 10. Intro and algorithms
Collection of papers on Software Verification.
Tutorial on extended static checking for Java.

Project assigments:

DART algorithm. From AST to CFG.
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:

Representative software analysis and verification tools.
Testing, symbolic execution, bug finding.
Verification conditions, extended static checking.
Invariant and ranking function generation.
Abstract interpretation.
Data flow analysis over finite domains.
Pointer and alias analysis.
Decision procedures. Predicate abstraction.
Counterexample-guided abstraction refinement. Interpolation.
Termination checking.
Context-free reachability, summarization.
Concurrency, race detection, atomicity.

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 %).