Differences between revisions 2 and 3
Revision 2 as of 2017-04-17 11:35:22
Size: 10098
Editor: rupak
Comment:
Revision 3 as of 2017-04-17 11:40:31
Size: 13593
Editor: rupak
Comment:
Deletions are marked like this. Additions are marked like this.
Line 2: Line 2:
Line 4: Line 3:
Line 8: Line 6:
  [[http://www.mpi-sws.org/~rupak/|Rupak Majumdar]] ([[mailto:rupak@mpi-sws.org|rupak@mpi-sws.org]])<<BR>>
 
Room 414, Building 26 (MPI-SWS)
  [[http://www.mpi-sws.org/~neider/|Daniel Neider]] ([[mailto:neider@mpi-sws.org|neider@mpi-sws.org]])<<BR>>
 
Room 315, Building 26 (MPI-SWS)
  . [[http://www.mpi-sws.org/~rupak/|Rupak Majumdar]] ( rupak@mpi-sws.org ) Room 414, Building 26 (MPI-SWS)
  . [[http://www.mpi-sws.org/~neider/|Daniel Neider]] ( neider@mpi-sws.org ) Room 315, Building 26 (MPI-SWS)
Line 13: Line 9:
  [[http://www.mpi-sws.org/~burcu/|Dr. Burcu Ozkan]] ([[mailto:burcu@mpi-sws.org|burcu@mpi-sws.org]])<<BR>>
  [[http://www.mpi-sws.org/~akschmuck/|Dr. Anne-Kathrin Schmuck]] ([[mailto:akschmuck@mpi-sws.org|akschmuck@mpi-sws.org]])<<BR>>
  . [[http://www.mpi-sws.org/~burcu/|Dr. Burcu Ozkan]] ( burcu@mpi-sws.org )
  . [[http://www.mpi-sws.org/~akschmuck/|Dr. Anne-Kathrin Schmuck]] ( akschmuck@mpi-sws.org )
Line 16: Line 12:
  Tuesdays 08:15-09:45 48-210 and Wednesdays 13:45-15:15 46-280<<BR>>
 * '''Tutorial''': Tuesday 10:00-11:30<<BR>>
  . Tuesdays 08:15-09:45 48-210 and Wednesdays 13:45-15:15 46-280
 * '''Tutorial''': Tuesday 10:00-11:30
Line 23: Line 19:
 * '''Syllabus and contents.'''
Line 24: Line 21:
  * '''Syllabus and contents.'''
We shall study automata on finite/infinite words and trees and their relationship to logic and computer-aided
verification of systems. 
We shall study automata on finite/infinite words and trees and their relationship to logic and computer-aided verification of systems.
Line 28: Line 23:
  * '''Intended Audience.'''
Computer science or math students with background in logic and theory of computation.
(Familiarity with basic algorithms, logic, and theory of computation will be assumed).
Talk to the instructor if you are not sure if you
have the background. We shall try to keep the class self-contained,
please attend the initial lecture for background material.
 * '''Intended Audience.'''
Line 35: Line 25:
Further, I expect you (1) have "mathematical maturity" (e.g., you should be comfortable with proofs and abstract reasoning);
(2) are interested in the material; and
(3) are willing to spend time outside of class in order to better understand the material presented in lectures.
Computer science or math students with background in logic and theory of computation. (Familiarity with basic algorithms, logic, and theory of computation will be assumed). Talk to the instructor if you are not sure if you have the background. We shall try to keep the class self-contained, please attend the initial lecture for background material.
Line 39: Line 27:
Further, I expect you (1) have "mathematical maturity" (e.g., you should be comfortable with proofs and abstract reasoning); (2) are interested in the material; and (3) are willing to spend time outside of class in order to better understand the material presented in lectures.
Line 40: Line 29:
 * '''Grading'''
Line 41: Line 31:
  * '''Grading'''
Grading will be based on a written, open-notes, final exam. Open notes means that you are free to bring your notes to the exam.
In order to appear for the exam, you have to turn in homework problems (to be
assigned approximately biweekly), write up lecture notes for two lectures, and present a result to the class.
Grading will be based on a written, open-notes, final exam. Open notes means that you are free to bring your notes to the exam. In order to appear for the exam, you have to turn in homework problems (to be assigned approximately biweekly), write up lecture notes for two lectures, and present a result to the class.
Line 47: Line 34:
  Class notes and research papers will be handed out.    . Class notes and research papers will be handed out.
Line 49: Line 36:
The text book
Michael Sipser, Introduction to the theory of computation,
contains the material we will cover in the first few weeks as well as the required background for the class.

The text book  Michael Sipser, Introduction to the theory of computation,  contains the material we will cover in the first few weeks as well as the required background for the class.
Line 56: Line 39:
  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.    . 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.
Line 58: Line 41:
  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.   . 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.
  .
Line 60: Line 44:
== 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.
== Announcements ==
 * The first lecture is on April 18, 2017.
Line 66: Line 48:

||<: 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) || || ||
||<rowbgcolor="&quot" rowstyle="#B7AFA3&quot"2% style="&quot;font-weight:bold; &quot; ;text-align:center"># ||<4%  style="&quot;font-weight:bold; &quot; ;text-align:center">Date ||<30%  style="&quot;font-weight:bold; &quot; ;text-align:center">Course topic / lecture ||<20%  style="&quot;font-weight:bold; &quot; ">Homework ||<35%  style="&quot;font-weight:bold; &quot; ">Materials ||<9%  style="&quot;font-weight:bold; &quot; ">Video ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L1 ||<style="text-align:center">April 23 ||<style="text-align:center">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="&quot" rowstyle="#C1DAD6&quot"style="text-align:center">- ||<style="text-align:center">April 25 || || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L2 ||<style="text-align:center">April 28 ||<style="text-align:center">Preliminaries: graph algorithms, automata theory ||[[attachment:hw1.pdf|Homework 1.]] Need not be turned in. ||[[attachment:Lecture2.pdf|Lecture notes]] || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L3 ||<style="text-align:center">April 30 ||<style="text-align:center">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="&quot" rowstyle="#C1DAD6&quot"style="text-align:center">T1 ||<style="text-align:center">May 2 ||<style="text-align:center">Solutions to Homework 1. || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L4 ||<style="text-align:center">May 5 ||<style="text-align:center">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="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L5 ||<style="text-align:center">May 7 ||<style="text-align:center">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="&quot" rowstyle="#C1DAD6&quot"style="text-align:center">T2 ||<style="text-align:center">May 9 ||<style="text-align:center">Q & A || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L6 ||<style="text-align:center">May 12 ||<style="text-align:center">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="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L7 ||<style="text-align:center">May 14 ||<style="text-align:center">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="&quot" rowstyle="#C1DAD6&quot"style="text-align:center">T3 ||<style="text-align:center">May 16 ||<style="text-align:center">Q & A || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L8 ||<style="text-align:center">May 19 ||<style="text-align:center">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="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L9 ||<style="text-align:center">May 21 ||<style="text-align:center">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="&quot" rowstyle="#C1DAD6&quot"style="text-align:center">T4 ||<style="text-align:center">May 23 ||<style="text-align:center">Q & A || || ||[[http://www.mpi-sws.org/seminars/vrs/2014-05-23_vrs.mp4|MP4 (313 MB)]] ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L10 ||<style="text-align:center">May 26 ||<style="text-align:center">Symbolic execution. || ||[[attachment:cacm13.pdf|Cadar, Sen. Symbolic execution for software testing: Three decades later.]] || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L11 ||<style="text-align:center">May 28 ||<style="text-align:center">Inductive invariants. Abstraction. || || || ||
||<rowbgcolor="&quot" rowstyle="#C1DAD6&quot"style="text-align:center">T5 ||<style="text-align:center">May 30 ||<style="text-align:center">Solutions to Homework 2. || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L12 ||<style="text-align:center">June 2 ||<style="text-align:center">Predicate abstraction and CEGAR. || ||[[attachment:SoftwareModelChecking.pdf|Survey on software model checking.]] || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L13 ||<style="text-align:center">June 4 ||<style="text-align:center">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="&quot" rowstyle="#C1DAD6&quot"style="text-align:center">T6 ||<style="text-align:center">June 6 ||<style="text-align:center">Q & A || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">- ||<style="text-align:center">June 9 ||<style="text-align:center">Holiday (No lecture) || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L14 ||<style="text-align:center">June 11 ||<style="text-align:center">Interpolation-based model checking || ||[[attachment:McMillan-Interpolation.pdf|McMillan. Interpolation and SAT-based model checking.]] || ||
||<rowbgcolor="&quot" rowstyle="#C1DAD6&quot"style="text-align:center">T7 ||<style="text-align:center">June 13 ||<style="text-align:center">Discussing projects || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L15 ||<style="text-align:center">June 16 ||<style="text-align:center">Simulation and Bisimulation || ||[[attachment:partition.pdf|Partition refinement]] || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L16 ||<style="text-align:center">June 18 ||<style="text-align:center">Simulation and Bisimulation || || || ||
||<rowbgcolor="&quot" rowstyle="#C1DAD6&quot"style="text-align:center">T8 ||<style="text-align:center">June 20 ||<style="text-align:center">Solutions to Homework 3. || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L17 ||<style="text-align:center">June 23 ||<style="text-align:center">Well-structured Transition Systems || ||[[attachment:marktoberdorf-notes.pdf|Majumdar. Marktoberdorf 2013 lecture notes.]] || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">- ||<style="text-align:center">June 25 ||<style="text-align:center">Cancelled. || || || ||
||<rowbgcolor="&quot" rowstyle="#C1DAD6&quot"style="text-align:center">T9 ||<style="text-align:center">June 27 ||<style="text-align:center">Q & A || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L18 ||<style="text-align:center">June 30 ||<style="text-align:center">Example: Concurrent programs || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L19 ||<style="text-align:center">July 2 ||<style="text-align:center">Safe Temporal Logic (STL) ||[[attachment:hw4.pdf|Homework 4.]] Due July 9/July 16, 2014. ||[[attachment:stl.pdf|Notes on STL]] || ||
||<rowbgcolor="&quot" rowstyle="#C1DAD6&quot"style="text-align:center">T10 ||<style="text-align:center">July 4 ||<style="text-align:center">Q & A || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L20 ||<style="text-align:center">July 7 ||<style="text-align:center">Model checking STL || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L21 ||<style="text-align:center">July 9 ||<style="text-align:center">Safety vs liveness ||[[attachment:Endterm.pdf|Practice exam]] ||[[attachment:safetyvsliveness.pdf|Safety and liveness]] (We did not cover all the material) || ||
||<rowbgcolor="&quot" rowstyle="#C1DAD6&quot"style="text-align:center">- ||<style="text-align:center">July 11 ||<style="text-align:center">Cancelled || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L22 ||<style="text-align:center">July 14 ||<style="text-align:center">CTL || ||[[attachment:CTL.pdf|CTL]] (For reading about linear time logics and automata: [[attachment:automata.pdf|Automata-theoretic verification]] || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L23 ||<style="text-align:center">July 16 ||<style="text-align:center">Model checking CTL ||[[attachment:exam-solutions.pdf|Solutions to the Practice Exam]] || || ||
||<rowbgcolor="&quot" rowstyle="#C1DAD6&quot"style="text-align:center">T11 ||<style="text-align:center">July 18 ||<style="text-align:center">Solutions to Homework 4. '''Moved to 10:00 am!''' || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">- ||<style="text-align:center">July 21 ||<style="text-align:center">No lecture (preperation time for project presentations) || || || ||
||<rowbgcolor="&quot" rowstyle="#F5FAFA&quot"style="text-align:center">L24 ||<style="text-align:center">July 23 ||<style="text-align:center">Project presentations || || || ||
||<rowbgcolor="&quot" rowstyle="#C1DAD6&quot"style="text-align:center">T12 ||<style="text-align:center">July 25 ||<style="text-align:center">Preparation for exam ||[[attachment:hw5.pdf|Homework 5.]] (No due date) || || ||

Course: Advanced Automata Theory

Summer 2017

Introduction

  • Syllabus and contents.

We shall study automata on finite/infinite words and trees and their relationship to logic and computer-aided verification of systems.

  • Intended Audience.

Computer science or math students with background in logic and theory of computation. (Familiarity with basic algorithms, logic, and theory of computation will be assumed). Talk to the instructor if you are not sure if you have the background. We shall try to keep the class self-contained, please attend the initial lecture for background material.

Further, I expect you (1) have "mathematical maturity" (e.g., you should be comfortable with proofs and abstract reasoning); (2) are interested in the material; and (3) are willing to spend time outside of class in order to better understand the material presented in lectures.

  • Grading

Grading will be based on a written, open-notes, final exam. Open notes means that you are free to bring your notes to the exam. In order to appear for the exam, you have to turn in homework problems (to be assigned approximately biweekly), write up lecture notes for two lectures, and present a result to the class.

  • Textbook:

    • Class notes and research papers will be handed out.

The text book Michael Sipser, Introduction to the theory of computation, contains the material we will cover in the first few weeks as well as the required background for the class.

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

Announcements

  • The first lecture is on April 18, 2017.

Schedule

#

Date

Course topic / lecture

Homework

Materials

Video

L1

April 23

Introduction to formal verification

Lecture slides
De Millo, Lipton, and Perlis. Social processes and proofs of programs.

-

April 25

L2

April 28

Preliminaries: graph algorithms, automata theory

Homework 1. Need not be turned in.

Lecture notes

L3

April 30

Preliminaries: propositional logic

Lecture notes
Problem L (Labyrinth). Solution.
Try OCaml, Learn OCaml, Real World OCaml

T1

May 2

Solutions to Homework 1.

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:
The Reactive modules modeling language.
Invariant verification.
SPIN web page.

L5

May 7

Peterson's protocol. Heuristics for enumerative invariant verification. Symbolic invariant verification. Symbolic reachability.

Alur and Henzinger. Symbolic graph representation.

MPG (660 MB)

T2

May 9

Q & A

L6

May 12

Symbolic model checking with SAT

Malik and Weissenbacher. Boolean satisfiability solvers: Techniques and extensions.
Nieuwenhuis, Oliveras, and Tinelli. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T).

MPG (678 MB)

L7

May 14

Implementing a SAT Solver. BDDs.

Homework 2. Due May 28, 2014.

MP4 (529 MB)

T3

May 16

Q & A

L8

May 19

BDDs.

Bryant. Graph-based algorithms for Boolean function manipulation. (The BDD paper.)

MP4 (434 MB)

L9

May 21

SMT. Timed automata and difference constraints.

Project suggestions.
Alur, Parthasarathy. Decision problems for timed automata: A survey.

T4

May 23

Q & A

MP4 (313 MB)

L10

May 26

Symbolic execution.

Cadar, Sen. Symbolic execution for software testing: Three decades later.

L11

May 28

Inductive invariants. Abstraction.

T5

May 30

Solutions to Homework 2.

L12

June 2

Predicate abstraction and CEGAR.

Survey on software model checking.

L13

June 4

IC3.

Homework 3. Due June 18, 2014.

Bradley. SAT-based model checking without unrolling. (The IC3 paper.)
Somenzi, Bradley. IC3: Where monolithic and incremental meet. (The IC3 tutorial.)

T6

June 6

Q & A

-

June 9

Holiday (No lecture)

L14

June 11

Interpolation-based model checking

McMillan. Interpolation and SAT-based model checking.

T7

June 13

Discussing projects

L15

June 16

Simulation and Bisimulation

Partition refinement

L16

June 18

Simulation and Bisimulation

T8

June 20

Solutions to Homework 3.

L17

June 23

Well-structured Transition Systems

Majumdar. Marktoberdorf 2013 lecture notes.

-

June 25

Cancelled.

T9

June 27

Q & A

L18

June 30

Example: Concurrent programs

L19

July 2

Safe Temporal Logic (STL)

Homework 4. Due July 9/July 16, 2014.

Notes on STL

T10

July 4

Q & A

L20

July 7

Model checking STL

L21

July 9

Safety vs liveness

Practice exam

Safety and liveness (We did not cover all the material)

-

July 11

Cancelled

L22

July 14

CTL

CTL (For reading about linear time logics and automata: Automata-theoretic verification

L23

July 16

Model checking CTL

Solutions to the Practice Exam

T11

July 18

Solutions to Homework 4. Moved to 10:00 am!

-

July 21

No lecture (preperation time for project presentations)

L24

July 23

Project presentations

T12

July 25

Preparation for exam

Homework 5. (No due date)

Courses/AdvancedAutomataTheory-SS2017 (last edited 2018-03-29 06:38:49 by neider)