17377
Comment:
|
14817
|
Deletions are marked like this. | Additions are marked like this. |
Line 30: | Line 30: |
---- /!\ '''Edit conflict - other version:''' ---- ---- /!\ '''Edit conflict - other version:''' ---- ---- /!\ '''Edit conflict - your version:''' ---- ---- /!\ '''End of edit conflict''' ---- |
|
Line 43: | Line 35: |
* '''Text book''' The following text books cover most of the material: a. '''Michael Sipser''', ''Introduction to the theory of computation'', MIT Press |
|
Line 44: | Line 39: |
---- /!\ '''Edit conflict - other version:''' ---- ---- /!\ '''Edit conflict - your version:''' ---- 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. However, you may not use internet access on any device during an exam. |
b. '''Graedel, Thomas, Wilke''', '' [[https://link.springer.com/book/10.1007%2F3-540-36387-4|Automata, Logics, and Infinite Games]]'', Springer |
Line 48: | Line 41: |
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. |
In addition, we shall provide lecture notes, surveys, or research papers for topics not covered in these books. |
Line 51: | Line 43: |
---- /!\ '''End of edit conflict''' ---- | * '''Homework:''' Homework exercises will be handed out approximately every two weeks (weekday TBA). Your answers must be handed in until the day specified in the homework, at the beginning of the lecture. |
Line 53: | Line 47: |
---- /!\ '''Edit conflict - your version:''' ---- ---- /!\ '''End of edit conflict''' ---- * '''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. ---- /!\ '''Edit conflict - other version:''' ---- ---- /!\ '''Edit conflict - other version:''' ---- ---- /!\ '''Edit conflict - your version:''' ---- ---- /!\ '''End of edit conflict''' ---- |
|
Line 71: | Line 48: |
Students may collaborate on homeworks, but each student needs to individually write up a solution set and be prepared | Students may collaborate on homework assignments, but each student needs to individually write up a solution set and be prepared |
Line 77: | Line 54: |
* '''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 beginning of the lecture. ---- /!\ '''Edit conflict - other version:''' ---- ---- /!\ '''Edit conflict - your version:''' ---- * '''Teamwork and Academic Honesty''': 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. The work you submit in this course must be the result of your individual effort. You may discuss homework problems and general proof strategies or algorithms with other students in the course, but you must not collaborate in the detailed development or actual writing of problem sets. This implies that one student should never have in his or her possession a copy of all or part of another student's homework. It is your responsibility to protect your work from unauthorized access. In writing up your homework you are allowed to use any book, paper, or published material. However, you are not allowed to ask others for specific solutions, either in person or by using electronic forums such as newsgroups. Of course, during the administration of exams any form of cooperation or help is forbidden. Academic dishonesty has no place in a university; it wastes our time and yours, and it is unfair to the majority of students. Any dishonest behavior will be severely penalized and may lead to failure in the course. * '''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 beginning of the lecture. ---- /!\ '''End of edit conflict''' ---- ---- /!\ '''Edit conflict - your version:''' ---- ---- /!\ '''End of edit conflict''' ---- |
Course: Advanced Automata Theory
Summer 2017
Instructor:
Rupak Majumdar ( rupak@mpi-sws.org ) Room 414, Building 26 (MPI-SWS)
Daniel Neider ( neider@mpi-sws.org ) Room 315, Building 26 (MPI-SWS)
Teaching assistants:
Lectures:
- Tuesdays 08:15-09:45 48-210 and Wednesdays 13:45-15:15 46-280
Tutorial: Tuesday 10:00-11:30
Office hours: By appointment
Mailing list: TBD
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. However, you may not use internet access on any device during an 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.
Text book
The following text books cover most of the material:
Michael Sipser, Introduction to the theory of computation, MIT Press
b. Graedel, Thomas, Wilke, Automata, Logics, and Infinite Games, Springer
In addition, we shall provide lecture notes, surveys, or research papers for topics not covered in these books.
Homework:
Homework exercises will be handed out approximately every two weeks (weekday TBA). Your answers must be handed in until the day specified in the homework, at the beginning of the lecture.
Teamwork and Academic Honesty:
Students may collaborate on homework assignments, but each student needs to individually write up a solution set and be prepared to present it in class on the due date. The work you submit in this course must be the result of your individual effort. You may discuss homework problems and general proof strategies or algorithms with other students in the course, but you must not collaborate in the detailed development or actual writing of problem sets. This implies that one student should never have in his or her possession a copy of all or part of another student's homework. It is your responsibility to protect your work from unauthorized access. In writing up your homework you are allowed to use any book, paper, or published material. However, you are not allowed to ask others for specific solutions, either in person or by using electronic forums such as newsgroups. Of course, during the administration of exams any form of cooperation or help is forbidden. Academic dishonesty has no place in a university; it wastes our time and yours, and it is unfair to the majority of students. Any dishonest behavior will be severely penalized and may lead to failure in the course.
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 |
|
- |
April 25 |
|
|
|
|
L2 |
April 28 |
Preliminaries: graph algorithms, automata theory |
Homework 1. Need not be turned in. |
|
|
L3 |
April 30 |
Preliminaries: propositional logic |
|
Lecture notes |
|
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: |
|
L5 |
May 7 |
Peterson's protocol. Heuristics for enumerative invariant verification. Symbolic invariant verification. Symbolic reachability. |
|
||
T2 |
May 9 |
Q & A |
|
|
|
L6 |
May 12 |
Symbolic model checking with SAT |
|
Malik and Weissenbacher. Boolean satisfiability solvers: Techniques and extensions. |
|
L7 |
May 14 |
Implementing a SAT Solver. BDDs. |
Homework 2. Due May 28, 2014. |
|
|
T3 |
May 16 |
Q & A |
|
|
|
L8 |
May 19 |
BDDs. |
|
Bryant. Graph-based algorithms for Boolean function manipulation. (The BDD paper.) |
|
L9 |
May 21 |
SMT. Timed automata and difference constraints. |
|
Project suggestions. |
|
T4 |
May 23 |
Q & A |
|
|
|
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. |
|
|
|
L13 |
June 4 |
IC3. |
Homework 3. Due June 18, 2014. |
Bradley. SAT-based model checking without unrolling. (The IC3 paper.) |
|
T6 |
June 6 |
Q & A |
|
|
|
- |
June 9 |
Holiday (No lecture) |
|
|
|
L14 |
June 11 |
Interpolation-based model checking |
|
|
|
T7 |
June 13 |
Discussing projects |
|
|
|
L15 |
June 16 |
Simulation and Bisimulation |
|
|
|
L16 |
June 18 |
Simulation and Bisimulation |
|
|
|
T8 |
June 20 |
Solutions to Homework 3. |
|
|
|
L17 |
June 23 |
Well-structured Transition Systems |
|
|
|
- |
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. |
|
|
T10 |
July 4 |
Q & A |
|
|
|
L20 |
July 7 |
Model checking STL |
|
|
|
L21 |
July 9 |
Safety vs liveness |
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 |
|
|
|
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) |
|
|