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:

  • Wednesday, 15:30-16:30 (Room 515, Building 26) or 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.

    Note: The permission to take the exam is derived from this year's homework. Having taking the course before does not count!

• 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.

• Logistics of Homwork:

  • Homework exercises will be handed out every two weeks (weekday TBA). Your answers must be handed in until the following Wednesday, 12:00pm (i.e., at noon). Answers can be handed in by e-mail or personally to any of the teaching assistants.

Schedule