Course: Verification of Reactive Systems

Summer 2014

• Instructor:

  • Rupak Majumdar (rupak@mpi-sws.org)
    Room 414, Building 26 (MPI-SWS)

• Teaching assistants:

  • Johannes Kloos (jkloos@mpi-sws.org)
    Filip Niksic (fniksic@mpi-sws.org)
    Room 515, Building 26 (MPI-SWS)

• Lectures:

  • Monday, Wednesday 08:15-09:45
    Room 111, Building 26 (MPI-SWS)

• Tutorial:

  • Friday 15:30-17:00
    Room 111, Building 26 (MPI-SWS)

• Office hours:

  • By appointment

• Mailing list:

  • https://lists.mpi-sws.org/listinfo/vrs14

• Background survey:

  • Please fill this background survey: https://de.surveymonkey.com/s/FDFGZLW

Introduction

This course focuses on the theory and practice of computer-aided verification, with an emphasis on software verification.

• Prerequisites:

  • The course requires basic knowledge of algorithms, data structures, automata theory, computational complexity, and propositional logic. For example, you should know what it means for a formula to be satisfiable, how to determinize a finite automaton, what is depth first search, and what P and NP means. If you are not familiar with these concepts, please attend the two initial lectures on background material.

• Textbook:

  • Class notes and research papers will be handed out.

• Grading:

  • Grades will be awarded on the basis of a final exam. Permission to take the final exam will be given based on your performance in homework assignments and a project paper.

• Projects:

  • Potential project topics, both theoretical and experimental, will be announced during the first few weeks of the course. Any suggestions for designing your own project according to your interests are very welcome. Every project will require a mentor. Projects will involve either surveying a field in depth, or using state of the art model checkers to verify large systems of interest, or to extend the capabilities of existing model checkers by implementing new algorithms or proving new theorems.

• Teamwork:

  • Students may collaborate on homeworks, but each student needs to individually write up a solution set and be prepared to present it in class on the due date. Projects must be done in groups, but each person should have a clearly identifiable responsibility.

Lecture Notes

• Lecture 1 (Wednesday, April 23)

  • Introduction to formal verification
    Lecture Slides
    De Millo, Lipton, and Perlis. Social processes and proofs of programs.

• Lecture 2 (Monday, April 28)

  • Preliminaries: graph algorithms, automata theory.
    Lecture Notes
    Homework 1 is available. This need not be turned in.

• Lecture 3 (Wednesday, April 30)

  • Preliminaries: propositional logic.
    For amusement (or practicing OCaml): Problem L (Labyrinth) from IPSC 2013. Solution.

• Lecture 4 (Monday, May 5)

  • The invariant verification problem. Enumerative invariant verification. Depth first search. Spin.
    Notes from an unpublished text book by Rajeev Alur and Tom Henzinger:

    • The Reactive modules modeling language
      Invariant verification

    The SPIN web page.