CS 7430: Formal Specification, Verification, and Synthesis, Fall 2020

Khoury College of Computer Sciences
Northeastern University

Instructor: Prof. Stavros Tripakis (also spelled Trypakis)

Class: Mon and Wed, 2:50-4:30PM, Hastings Suite 118

Office hours: WVH 340 or online (TBD), Mon and Wed 4:30-5:30PM, or by request


Introduction

Science is knowledge that helps us make predictions. This course is about the science of software and systems. What predictions can we make about the software that we write? Can we predict that our program will never crash? That its output will be correct? What does "correct" mean, exactly? And what predictions can we make about safety-critical, embedded, cyber-physical, and all sorts of other systems that heavily rely on software? This course covers the fundamentals in formal system modeling, specification, verification, and synthesis, with a focus on automated methods (model checking, computer-aided verification and synthesis).

This course is often cross-listed with CS4830 System Specification, Verification, and Synthesis.

Goals:

  1. Understand the fundamental concepts in modern system theory.
  2. Learn how to formally model systems and specify their correctness.
  3. Learn the basic algorithmic techniques for checking that a system satisfies its specification (model-checking).
  4. Learn the basic techniques for automated system synthesis.
  5. Be able to use model-checkers such as Spin and NuXMV.

Schedule

The schedule below will be updated as we go along:

Lecture #, Date
Topics, slides, code, other material
Suggested readings

Logistics

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: More advanced reading:

Software

Install and familiarize yourself with:

Forum

We will use the discussion forum on Canvas. 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 Canvas. The assignments are to be done either individually or by groups of 2-3 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 discussion 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 in-class exams.

Presentations

Every student will pick 1-2 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 hands-on 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: Graduate 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 disability-related 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.
Page maintained by Stavros Tripakis