Program Analysis, Verification, and Synthesis, Fall 2018
| Name | Office | Office Hours (also available by appointment) |
|
|---|---|---|---|
| Jeff Foster | 211 Halligan | jfoster@cs.tufts.edu | MW 1:15-2:00pm |
| Matthew Ahrens | matthew.ahrens at tufts |
| Location | 111A Halligan |
|---|---|
| Time | MW 3:00-4:15 |
| Midterm | Wed, Oct 24, in class |
| Final | Available Dec 13-16 |
| Textbooks | There are no required or recommended texts. See the resources page for useful online links. |
The idea of software—the interchangeable instructions that control general-purpose computing devices—is one of the major breakthroughs of Computer Science. While we often think of software as human-generated text, in fact from the earliest days of computing, when compiler technology was first developed, researchers have been exploring ways to manipulate and reason about software algorithmically.
In this class, we will study three closely related topics that arose out of this research. We will begin with program analysis, which initially was developed to enable compilers to perform optimization. Today, program analyses are also used to solve a range of software engineering problems, including finding bugs and security vulnerabilities. Next, we will study program verification, which aims to prove that programs are correct. In recent years, researchers have built verified compilers, operating systems, cryptography libraries, and others. Finally, we will study program synthesis, which searches for a program satisfying a specification. Researchers have demonstrated synthesis of synchronization for high-performance parallel code, program inverses, fast Fourier transforms, and more. Program synthesis even underlies the Flash Fill feature of Microsoft Excel.
Each of these topics could be a course on its own, so the goal of this class is to give students a broad overview of these areas and the relationships between them. Throughout the course, students will design an implement basic program analysis, verification, and synthesis tools, and study the theory behind them.
| Week | Monday | Wednesday | |
|---|---|---|---|
| Sep 3 | Introduction OCaml Project 1 | ||
| Sep 10 | Lambda Calculus | Intermediate Representations Optimization | |
| Sep 17 | Data Flow Analysis | Dataflow Analysis Project 2 | |
| Sep 24 | Dataflow Analysis | Dataflow Analysis Static Single Assignment Form | |
| Oct 1 | Static Single Assignment Form Abstract Interpretation | Abstract Interpretation Project 3 | |
| Oct 8 | (Tue, Oct 9) Type Inference | Type Inference Subtype Inference | |
| Oct 15 | Subtype Inference | Symbolic Execution | |
| Oct 22 | Symbolic Execution | Midterm | |
| Oct 29 | Axiomatic Semantics Project 4 | Axiomatic Semantics | |
| Nov 5 | Axiomatic Semantics Exercises (Sample solutions) | Axiomatic Semantics | |
| Nov 12 | Veteran's Day -- No class | Guest Lecture - Sam Guyer | |
| Nov 19 | Axiomatic Semantics Separation Logic (see Resources) | Thanksgiving -- No class | |
| Nov 26 | Program Synthesis (Lecs 1-4) | Guest Lecture: Kathleen Fisher Project 5 | |
| Dec 3 | Program Synthesis (Lecs 7-10) | Program Synthesis (Lec 14) Adaptive Concretization Program Inversion PROSE | |
| Dec 10 | Retrospective Discussion | (Reading Period) |
COMP 105, graduate standing, or instructor consent. If you are not sure whether you meet the prerequisites for the course, please contact the instructor.
Below is an approximate list of topics for class. The exact topics will be determined based on the pace of the class.
Office hours for the instructional staff will be posted on the course web page a few days into the semester.
While we will provide assistance with assignments during office hours, you are responsible for developing and debugging your own programs. Do not rely on the instructional staff to make your project work.
Important announcements will be made in class or on Piazza. Please make it a habit to check Piazza daily, and/or sign up to receive email when updates are posted to Piazza. You may also use the class web forum to ask general questions of interest to the class as a whole, e.g., administrative issues or project clarification questions. Please do not post any information that would violate the University's Academic Integrity Policy.
You are responsible for all material discussed in class and posted on the class web page, including announcements, deadlines, policies, etc. Your final course grade will be determined according to the following percentages:
| Projects/homework | 50% |
| Midterm | 24% |
| Final | 25% |
| Meet your professor | 1% |
Any request for reconsideration of any grading on coursework must be submitted within one week of when it is returned. Exam regrading requests must be made in writing. Any coursework submitted for reconsideration may be regraded in its entirety, which could result in a lower score if warranted.
Final course grades will be curved as necessary, based on each student's total numeric score for all coursework at the end of the semester. Important: Completing the programming assignments is an essential part of the course. Therefore, we may fail any student who does not make a good-faith attempt on all course projects, regardless of the student's performance or scores on the other coursework.
Projects must be submitted electronically following the instructions given in class. Projects may not be submitted by any other means (e.g., please do not email your projects to us). It is your responsibility to test your program and verify that it works properly before submitting. All projects are due at 11:59pm on the day indicated on the project assignment, according to the submission server's internal clock.
Projects may be submitted up to 24 hours late for a 10% penalty. For example, a project that would earn 90 points for an on-time submission will earn 81 (which is 90 times 0.90) if submitted late. Note that your project score as it appears on the project submission server will not include any late penalties. Any penalties will be incorporated into the final project grade on the grade server.
The class includes a midterm and a final exam. Tentative dates for the exams will be posted on the class web site. The exact dates will be confirmed later. We will let you know the exact dates well in advance.
The Academic Resource Center offers a range of services for students.
Tufts University values the diversity of our students, staff, and faculty, recognizing the important contribution each student makes to our unique community. Tufts is committed to providing equal access and support to all qualified students through the provision of reasonable accommodations so that each student may fully participate in the Tufts experience. If you have a disability that requires reasonable accommodations, please contact the Student Accessibility Services office to make an appointment with an SAS representative to determine appropriate accommodations. Please be aware that accommodations cannot be enacted retroactively, making timeliness a critical aspect for their provision.
Please also contact the instructor to discuss any necessary accommodations.
You are expected to attend class regularly, complete course assignments on time, and take exams at the scheduled times. If you are unable to fulfill these requirements due to absence for a good reason, the instructor will excuse the absence and provide accommodation. Events that justify an excused absence include:
It is your responsibility to inform the instructor in advance of intended religious observances. Notice must be provided immediately upon an exam date being announced or confirmed for an absence to be excused.
The policies for excused absences do not apply to project assignments. Projects will be assigned with sufficient time to allow students to carry out the work even with other responsibilities. In cases of extremely serious documented illness of lengthy duration or other protracted, severe emergency situations, the instructor may consider extensions depending on the specific cirucmstances.
Absences stemming from job interviews, traffic or transportation problems, personal travel, and similar will not be excused.
The university's Academic Integrity Policy will be strictly enforced.
Unless otherwise specified, programming projects are to be written individually. Therefore, cooperation or use of unauthorized materials on projects is a violation of the Academic Integrity Policy. Project solutions may not be posted online. Any evidence of this, or of unacceptable use of computer accounts, use of unauthorized materials or cooperation on exams or quizzes, or other possible academic integrity violations will be reported.
For learning the course concepts, students are welcome to study together or to receive help from anyone else. You may discuss with others the project requirements, the features of the programming languages used, what was discussed in class and in the class web forum, and general syntax errors. Examples of questions that would be allowed are "Does a Java class definition end in a semicolon?" or "What does a 'class not found' error indicate?", because they convey no information about the contents of a project.
When it comes to actually writing a project assignment, other than help from the instructional staff a project must solely and entirely be your own work. Working with another student or individual, or using anyone else's work in any way except as noted in this paragraph, is a violation of the Academic Integrity Policy. You may not discuss design of any part of a project with anyone except the instructor or teaching assistants. Examples of questions you may not ask others might be "How did you implement this part of the project?" or "Please look at my code and help me find my stupid syntax error!". You may not use any disallowed source of information in creating either their project design or code. When writing projects you are free to use ideas or short fragments of code from published textbooks or publicly available information, but the specific source must be cited in a comment in the relevant section of the program.
Violations of the Code of Academic Integrity may include, but are not limited to:
If you have any question about a particular situation or source then consult with the instructor in advance. Should you have difficulty with a programming assignment you should see the instructional staff in office hours, and not solicit help from anyone else in violation of these rules.
Although every effort has been made to be complete and accurate, unforeseen circumstances arising during the semester could require the adjustment of any material given here. Consequently, given due notice to students, the instructor reserves the right to change any information on this syllabus or in other course materials.
Here are books you may be interested in if you want to go into much more depth on some of the class material, and in many cases beyond it. None of these is required for the class.