This Fall 2023, the graduate course CS 7430 Formal Specification, Verification, and Synthesis is cross-listed with the undergraduate course CS 4830 System Specification, Verification, and Synthesis.
Goals:
Course structure
Weekly 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 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 (as specified). 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
TBDPresentations
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 (TENTATIVE, SUBJECT TO CHANGE!)
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 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.