#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''':
  Monday, 15:30-16:30 (Room 515, Building 26) or by appointment
 * '''Mailing list''':
  https://lists.mpi-sws.org/listinfo/vrs14
{{{#!wiki comment
 * '''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!

  '''Exam dates''': July 28 and October 13, 2014
 * '''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 Homework:'''
  Homework exercises will be handed out every two weeks (weekday TBA). Your answers must be handed in until the day specified in the homework, at the end of the lecture. Answers can be handed in personally to any of the teaching assistants.

== Exam ==

 * The first exam will take place on July 28th, at 9:00am, in rooms 56-206 and 56-207.
 * The exam is an open-book exam: You may bring any notes and literature that you like.

== Schedule ==

||<: 2% rowbgcolor="#B7AFA3" style="font-weight: bold;"> # ||<: 4% style="font-weight: bold;"> Date ||<: 30% style="font-weight: bold;"> Course topic / lecture ||<20% style="font-weight: bold;"> Homework ||<35% style="font-weight: bold;"> Materials ||<9% style="font-weight: bold;"> Video ||
||<: rowbgcolor="#F5FAFA"> L1 ||<:> April 23 ||<:> Introduction to formal verification || || [[attachment:Lecture1.ppt|Lecture slides]]<<BR>>[[attachment:demillo.pdf|De Millo, Lipton, and Perlis. Social processes and proofs of programs.]] || ||
||<: rowbgcolor="#C1DAD6"> - ||<:> April 25 || || || || ||
||<: rowbgcolor="#F5FAFA"> L2 ||<:> April 28 ||<:> Preliminaries: graph algorithms, automata theory || [[attachment:hw1.pdf|Homework 1.]] Need not be turned in. || [[attachment:Lecture2.pdf|Lecture notes]] || ||
||<: rowbgcolor="#F5FAFA"> L3 ||<:> April 30 ||<:> Preliminaries: propositional logic || || [[attachment:Lecture3.pdf|Lecture notes]]<<BR>>[[http://ipsc.ksp.sk/2013/real/problems/l.html|Problem L (Labyrinth).]] [[https://github.com/fniksic/labyrinth|Solution]].<<BR>>[[http://try.ocamlpro.com|Try OCaml]], [[http://ocaml.org/learn/|Learn OCaml]], [[https://realworldocaml.org|Real World OCaml]] || ||
||<: rowbgcolor="#C1DAD6"> T1 ||<:> May 2 ||<:> Solutions to Homework 1. || || || ||
||<: rowbgcolor="#F5FAFA"> L4 ||<:> 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: <<BR>> [[attachment:CavBook-1.pdf|The Reactive modules modeling language.]]<<BR>>[[attachment:CavBook-2.pdf|Invariant verification.]]<<BR>>[[http://spinroot.com/|SPIN]] web page. || ||
||<: rowbgcolor="#F5FAFA"> L5 ||<:> May 7 ||<:> Peterson's protocol. Heuristics for enumerative invariant verification. Symbolic invariant verification. Symbolic reachability. || || [[attachment:CavBook-3.pdf|Alur and Henzinger. Symbolic graph representation.]] || [[http://www.mpi-sws.org/seminars/vrs/2014-05-07_vrs.mpg|MPG (660 MB)]] ||
||<: rowbgcolor="#C1DAD6"> T2 ||<:> May 9 ||<:> Q & A || || || ||
||<: rowbgcolor="#F5FAFA"> L6 ||<:> May 12 ||<:> Symbolic model checking with SAT || || [[attachment:Sharad Malik MOD Chapter.pdf|Malik and Weissenbacher. Boolean satisfiability solvers: Techniques and extensions.]]<<BR>>[[attachment:NieOT-JACM-06.pdf|Nieuwenhuis, Oliveras, and Tinelli. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T).]] || [[http://www.mpi-sws.org/seminars/vrs/2014-05-12_vrs.mpg|MPG (678 MB)]] ||
||<: rowbgcolor="#F5FAFA"> L7 ||<:> May 14 ||<:> Implementing a SAT Solver. BDDs. || [[attachment:hw2.pdf|Homework 2.]] Due May 28, 2014. || || [[http://www.mpi-sws.org/seminars/vrs/2014-05-14_vrs.mp4|MP4 (529 MB)]] ||
||<: rowbgcolor="#C1DAD6"> T3 ||<:> May 16 ||<:> Q & A || || || ||
||<: rowbgcolor="#F5FAFA"> L8 ||<:> May 19 ||<:> BDDs. || || [[attachment:ieeetc86.pdf|Bryant. Graph-based algorithms for Boolean function manipulation. (The BDD paper.)]] || [[http://www.mpi-sws.org/seminars/vrs/2014-05-19_vrs.mp4|MP4 (434 MB)]] ||
||<: rowbgcolor="#F5FAFA"> L9 ||<:> May 21 ||<:> SMT. Timed automata and difference constraints. || || [[attachment:Projects.pdf|Project suggestions.]]<<BR>>[[attachment:Timed Automata.pdf|Alur, Parthasarathy. Decision problems for timed automata: A survey.]] ||  ||
||<: rowbgcolor="#C1DAD6"> T4 ||<:> May 23 ||<:> Q & A || || || [[http://www.mpi-sws.org/seminars/vrs/2014-05-23_vrs.mp4|MP4 (313 MB)]] ||
||<: rowbgcolor="#F5FAFA"> L10 ||<:> May 26 ||<:> Symbolic execution. || || [[attachment:cacm13.pdf|Cadar, Sen. Symbolic execution for software testing: Three decades later.]] || ||
||<: rowbgcolor="#F5FAFA"> L11 ||<:> May 28 ||<:> Inductive invariants. Abstraction. || || || ||
||<: rowbgcolor="#C1DAD6"> T5 ||<:> May 30 ||<:> Solutions to Homework 2. || || || ||
||<: rowbgcolor="#F5FAFA"> L12 ||<:> June 2 ||<:> Predicate abstraction and CEGAR. || || [[attachment:SoftwareModelChecking.pdf|Survey on software model checking.]] || ||
||<: rowbgcolor="#F5FAFA"> L13 ||<:> June 4 ||<:> IC3. || [[attachment:hw3.pdf|Homework 3.]] Due June 18, 2014. || [[attachment:ic3_bradley.pdf|Bradley. SAT-based model checking without unrolling. (The IC3 paper.)]]<<BR>>[[attachment:ic3_tut.pdf|Somenzi, Bradley. IC3: Where monolithic and incremental meet. (The IC3 tutorial.)]] || ||
||<: rowbgcolor="#C1DAD6"> T6 ||<:> June 6 ||<:> Q & A || || || ||
||<: rowbgcolor="#F5FAFA"> - ||<:> June 9 ||<:>Holiday (No lecture) || || || ||
||<: rowbgcolor="#F5FAFA"> L14 ||<:> June 11 ||<:> Interpolation-based model checking || || [[attachment:McMillan-Interpolation.pdf|McMillan. Interpolation and SAT-based model checking.]] || ||
||<: rowbgcolor="#C1DAD6"> T7 ||<:> June 13 ||<:> Discussing projects || || || ||
||<: rowbgcolor="#F5FAFA"> L15 ||<:> June 16 ||<:> Simulation and Bisimulation || || [[attachment:partition.pdf|Partition refinement]] || ||
||<: rowbgcolor="#F5FAFA"> L16 ||<:> June 18 ||<:> Simulation and Bisimulation || || || ||
||<: rowbgcolor="#C1DAD6"> T8 ||<:> June 20 ||<:> Solutions to Homework 3. || || || ||
||<: rowbgcolor="#F5FAFA"> L17 ||<:> June 23 ||<:> Well-structured Transition Systems || || [[attachment:marktoberdorf-notes.pdf|Majumdar. Marktoberdorf 2013 lecture notes.]] || ||
||<: rowbgcolor="#F5FAFA"> - ||<:> June 25 ||<:> Cancelled. || || || ||
||<: rowbgcolor="#C1DAD6"> T9 ||<:> June 27 ||<:> Q & A || || || ||
||<: rowbgcolor="#F5FAFA"> L18 ||<:> June 30 ||<:> Example: Concurrent programs || || || ||
||<: rowbgcolor="#F5FAFA"> L19 ||<:> July 2 ||<:> Safe Temporal Logic (STL) || [[attachment:hw4.pdf|Homework 4.]] Due July 9/July 16, 2014. || [[attachment:stl.pdf|Notes on STL]] || ||
||<: rowbgcolor="#C1DAD6"> T10 ||<:> July 4 ||<:> Q & A || || || ||
||<: rowbgcolor="#F5FAFA"> L20 ||<:> July 7 ||<:> Model checking STL || || || ||
||<: rowbgcolor="#F5FAFA"> L21 ||<:> July 9 ||<:> Safety vs liveness || [[attachment:Endterm.pdf|Practice exam]] || [[attachment:safetyvsliveness.pdf|Safety and liveness]] (We did not cover all the material) || ||
||<: rowbgcolor="#C1DAD6"> - ||<:> July 11 ||<:> Cancelled || || || ||
||<: rowbgcolor="#F5FAFA"> L22 ||<:> July 14 ||<:> CTL || || [[attachment:CTL.pdf|CTL]] (For reading about linear time logics and automata: [[attachment:automata.pdf|Automata-theoretic verification]] || ||
||<: rowbgcolor="#F5FAFA"> L23 ||<:> July 16 ||<:> Model checking CTL || [[attachment:exam-solutions.pdf|Solutions to the Practice Exam]] || || ||
||<: rowbgcolor="#C1DAD6"> T11 ||<:> July 18 ||<:> Solutions to Homework 4. '''Moved to 10:00 am!''' || || || ||
||<: rowbgcolor="#F5FAFA"> - ||<:> July 21 ||<:> No lecture (preperation time for project presentations) || || || ||
||<: rowbgcolor="#F5FAFA"> L24 ||<:> July 23 ||<:> Project presentations || || || ||
||<: rowbgcolor="#C1DAD6"> T12 ||<:> July 25 ||<:> Preparation for exam || [[attachment:hw5.pdf|Homework 5.]] (No due date) || || ||