Differences between revisions 1 and 14 (spanning 13 versions)
⇤ ← Revision 1 as of 2014-04-29 08:54:09 →
Size: 28
Editor: fniksic
Comment:
← Revision 14 as of 2014-05-02 19:45:11 → ⇥
Size: 3829
Editor: jkloos
Comment: Added lecture notes.
Deletions are marked like this. Additions are marked like this.
Line 1: Line 1:
Describe Courses/VRS here. #acl fniksic,jkloos,rupak:read,write,delete,revert,admin All:read

= Course: Verification of Reactive Systems =

'''Summer 2014'''

 * '''Instructor''':
  [[http://www.mpi-sws.org/~rupak/|Rupak Majumdar]] ([[mailto:rupak@mpi-sws.org|rupak@mpi-sws.org]])<<BR>>
  Room 414, Building 26 (MPI-SWS)
 * '''Teaching assistants''':
  [[http://www.mpi-sws.org/~jkloos/|Johannes Kloos]] ([[mailto:jkloos@mpi-sws.org|jkloos@mpi-sws.org]])<<BR>>
  [[http://www.mpi-sws.org/~fniksic/|Filip Niksic]] ([[mailto:fniksic@mpi-sws.org|fniksic@mpi-sws.org]])<<BR>>
  Room 515, Building 26 (MPI-SWS)
 * '''Lectures''':
  Monday, Wednesday 08:15-09:45<<BR>>
  Room 111, Building 26 (MPI-SWS)
 * '''Tutorial''':
  Friday 15:30-17:00<<BR>>
  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<<BR>>
  [[attachment:Lecture1.ppt|Lecture Slides]]<<BR>>
  De Millo, Lipton, and Perlis. [[attachment:demillo.pdf|Social processes and proofs of programs]].
 * '''Lecture 2''' (Monday, April 28)
  Preliminaries: graph algorithms, automata theory.<<BR>>
  [[attachment:Lecture2.pdf|Lecture Notes]]<<BR>>
  [[attachment:hw1.pdf|Homework 1]] is available. This need not be turned in.
 * '''Lecture 3''' (Wednesday, April 30)
  Preliminaries: propositional logic.<<BR>>
  For amusement (or practicing OCaml):
  [[http://ipsc.ksp.sk/2013/real/problems/l.html|Problem L (Labyrinth)]] from [[http://ipsc.ksp.sk|IPSC]] 2013. [[https://github.com/fniksic/labyrinth|Solution]].
 * '''Lecture 4''' (Monday, May 5)
  The invariant verification problem. Enumerative invariant verification. Depth first search. Spin.<<BR>>
  Notes from an unpublished text book by Rajeev Alur and Tom Henzinger:
   [[attachment:CavBook-1.pdf|The Reactive modules modeling language]]<<BR>>
   [[attachment:CavBook-2.pdf|Invariant verification]]
  The [[http://spinroot.com/|SPIN]] web page.

Course: Verification of Reactive Systems

Summer 2014

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

Courses/VRS (last edited 2014-07-24 13:41:45 by jkloos)