Software Model Checking
Advanced course in Winter 2007/08. 6 CP.
Instructor: Andrey Rybalchenko
- (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:
- (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.
- 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.
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.
Representative software analysis and verification tools.
Testing, symbolic execution, bug finding.
Verification conditions, extended static checking.
Invariant and ranking function generation.
Data flow analysis over finite domains.
Pointer and alias analysis.
Decision procedures. Predicate abstraction.
Counterexample-guided abstraction refinement. Interpolation.
Context-free reachability, summarization.
Concurrency, race detection, atomicity.
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 %).