Goals:
Lecture #, Date 
Topics, slides, code, other material 
Suggested readings 
Class 01, 4 Sep 2019 
1. Introduction; The science of software and systems; Logistics; Slides: 01intro.pdf  Chapter 1 of BaierKatoen; CACM paper How Amazon Web Services Uses Formal Methods 
Class 02, 9 Sep 2019 
2. Systems; System design methods;
Slides: 02systems.pdf
3. Finite state machines; Modeling FSMs in nuXmv; Slides: 03statemachines.pdf 
RAND report Driving to Safety; Lamport paper Computation and State Machines 
Class 03, 11 Sep 2019 
4. Transition systems; Promela and Spin; Slides: 04transitionsystems.pdf  Chapter 2 of BaierKatoen 
Class 04, 16 Sep 2019 
5. System composition; Synchronous composition; Slides: 05synchronous.pdf  Chapter 2 of BaierKatoen; Malik paper Analysis of Cyclic Combinational Circuits 
Class 05, 18 Sep 2019 
6. Asynchronous composition;
Slides: 06asynchronous.pdf;
7. The statespace explosion problem; Slides: 07stateexplosion.pdf 
Chapter 2 of BaierKatoen; AlurTripakis paper Automatic Synthesis of Distributed Protocols 
Class 06, 23 Sep 2019 
8. Fairness; Slides: 08fairness.pdf  Chapter 3 of BaierKatoen; PitermanPnueli paper Temporal Logic and Fair Discrete Systems; 
Class 07, 25 Sep 2019 
9. Specification; Temporal logic; LTL; Slides: 09specltl.pdf  Chapter 5 of BaierKatoen (up to 5.2); A primer on logic (draft) 
Class 08, 30 Sep 2019 
9. LTL continued: The LTL modelchecking problem;
Invariants in LTL; LTL in Spin;
Slides: 09specltl.pdf
10. Safety and liveness; Slides: 10safetyliveness.pdf 
AlpernSchneider paper Defining Liveness; 
Class 09, 2 Oct 2019 
11. CTL; Slides: 11ctl.pdf  Chapter 6 of BaierKatoen (up to 6.4); 
Class 10, 7 Oct 2019 
Homework 2 solution review;  
Class 11, 9 Oct 2019 
12. Reachability analysis; Slides: 12reachability.pdf  BaierKatoen, Section 3.3.1 and Appendix A.4 
Class 12, 16 Oct 2019 
Exam 1  
Class 13, 21 Oct 2019 
13. Symbolic methods; Symbolic representation of state spaces; Symbolic reachability; Slides: 13symbolic.pdf  BaierKatoen, Sections 6.7.1 and 6.7.2 
Class 14, 23 Oct 2019 
14. Binary Decision Diagrams; Slides: 14bdd.pdf  BaierKatoen, Sections 6.7.3 and 6.7.4 
Class 15, 28 Oct 2019 
Guest lecture by Sergio Campos on compositional methods and case studies; Slides: campos1motivation.pdf, campos2compositional.pdf, campos3vod.pdf, campos4insilicoexps.pdf  
Class 16, 30 Oct 2019 
15. CTL model checking; Slides: 15ctlmodelchecking.pdf  BaierKatoen, Section 6.4 
Class 17, 4 Nov 2019 
16. Automata: Finite automata; Omega automata; Buchi automata; Slides: 16automata.pdf  BaierKatoen, Sections 4.1 and 4.3 
Class 18, 6 Nov 2019 
17. LTL model checking; Slides: 17ltlmodelchecking.pdf  BaierKatoen, Section 5.2 
Class 19, 13 Nov 2019 
Homework and exam review. 18. Bounded model checking; Slides: 18bmc.pdf 

Class 20, 18 Nov 2019 
19. Controller Synthesis: Slides: 19controllersynthesis.pdf  AlurTripakis SIGACT paper "Automatic Synthesis of Distributed Protocols", 
Class 21, 20 Nov 2019 
20. Program Synthesis: Slides: 20programsynthesis.pdf  
Class 22, 25 Nov 2019 
21. Homework 4 exhibit; Parting thoughts. Slides: 99bye.pdf  
Class 23, 2 Dec 2019 
22. Project and paper presentations  
Class 24, 4 Dec 2019 
23. Project and paper presentations 
Course structure
Biweekly lectures and homeworks. At the end of the semester, we will have student presentations (paper presentations by both undergraduate and graduate students; plus project presentations by graduate students).Textbooks
We will not follow a specific textbook. However, the following textbooks are useful readings:Software
Install and familiarize yourself with:Forum
We will use this piazza forum to post questions, answers, thoughts, links, etc, related to the course. Please check it at least every few days and participate actively. You can use it to post questions related to the projects or homeworks in this course. Specifically, clarification questions about the homework, such as "What does XYZ in homework 3 question 2.b mean?" should be posted to the forum. Also questions about the material covered lectures, e.g., "Is this LTL formula satisfied on this transition system? Why or why not?" should be posted to the forum.Never be afraid to ask questions: ask in the forum, ask during class. Always remember: there are no stupid questions!
Homeworks
Homework assignments are posted on Blackboard. The assignments are to be done either individually or by groups of 23 students. To collaborate effectively, you should all be involved in all aspects of the homework problems. Homeworks will be marked 20 points off per day that they are late, up to 2 days. Important: You are responsible for finding a partner (e.g., using the piazza forum, or before/after lectures). Homework submission instructions will be made available in class. Any requests for grade changes or regrading must be made within 7 days of when the work was returned. To ask for a regrade, specify (a) the problem or problems you want to be regraded, and (b) for each of these problems, why you think the problem was misgraded.Exams
There will be two exams. The first exam will be given approximately halfway through the semester and the second exam will be given towards the end of the semester. They will both be inclass exams.Presentations
Every student will pick 12 relevant research papers that they find interesting and will read and present to the class. The presentation should include a motivation, it should relate the presented material to the material covered in class and it should explain why the topic is important and interesting. We will schedule the presentations later and determine their length and dates. The instructor will recommend some papers but students are encouraged to search and propose papers that they want to present themselves. Important: presentations are done individually, not in groups.Projects
Projects are required only for graduate students. Graduate students have to propose a project that the instructor will review and approve (some suggestions will be provided by the instructor but as with presentations, students are encouraged to propose their own projects). Projects allow you to gain handson experience on a topic of interest. We suggest first choosing a project and then selecting papers for your presentation related to your project topic. Your project can be theoretical, say coming up with a verification or synthesis algorithm, or they can involve the implementation of an interesting algorithm, or they can involve the use and evaluation of existing tools (e.g., modeling and verifying some protocol).Grading
Undergraduate students:Academic Integrity
It's OK to ask someone about the concepts, algorithms, or approaches needed to do the assignments. We encourage you to do so; both giving and taking advice will help you to learn. However, what you turn in must be your own, or for projects, your group's own work; copying other people's code, solution sets, or from any other sources is strictly prohibited, unless you are explicitly given permission to do so. In particular, looking at other solutions (e.g., someone else's solution to a similar project) is a direct violation of our academic integrity policy. The project assignments must be entirely the work of the students turning them in. If you have any questions about using a particular resource, ask me. All students are subject to the Northeastern Academic Integrity policy. All cases of suspected plagiarism or other academic dishonesty will be referred to the Office of Student Conduct and Conflict Resolution (OSCCR) and to the college. In addition to any penalties imposed by OSSCR and the college, each violation of the academic integrity policy will result in a full grade reduction for the class in addition to a zero grade on any affected assignments, projects, exams or graded material.Accommodations for Students with Disabilities
If you have a disabilityrelated need for reasonable academic accommodations in this course and have not yet met with a Disability Specialist, please visit the Northeastern Disability Resource Center and follow the outlined procedure to request services. If the Disability Resource Center has formally approved you for an academic accommodation in this class, please present the instructor with your "Professor Notification Letter" during the first week of the semester, so that we can address your specific needs as early as possible.