CSCI 625: Program Synthesis and Computer-Aided Verification

Spring 2022

Logistics

Classes: Mondays and Wednesdays, 3:30pm–5:20pm
SOS B48 · https://usc.zoom.us/j/99799680225
Note the Zoom classroom we will be using for class!
Scratchpad: Click here
Piazza: https://piazza.com/usc/spring2022/csci625
Instructor: Mukund Raghothaman (raghotha@usc.edu)
Office hours: Fridays, 3:30pm–5:20pm, or by appointment · https://usc.zoom.us/j/93842877280

Course Description

This course is about the theory and practice of algorithmic program verification. We will discuss how programmers can prove that their code is correct, and how this process may be automated. We will study SAT and SMT solvers, and learn how to use them and how they work. These are sophisticated reasoning engines, and their use increasingly impacting other areas of computer science. We will see how they can be used to build automatic program synthesizers, which produce code that is correct-by-construction. [Syllabus]

Prerequisites: First, the course will expect a certain amount of mathematical maturity from its students, at least at the level of CSCI 170, and preferably at the level of CSCI 270. Second, we will be reasoning about code: we expect that the student will already be proficient in writing it.

Note: The syllabus and schedule listed on this webpage are tentative, and may be updated as the course progresses. Please check back regularly!

Grading

The course will consist of four homework assignments and an open-ended project, graded equally. The homework assignments are intended to develop familiarity with the material covered in class. In the project, you will apply and extend ideas from the course to a research problem of your choice. The project may be done either alone or in pairs. Please consult the instructor for feedback while choosing project topics.

Annonucements

Readings

  1. Daniel Kroening and Ofer Strichman. Decision Procedures: An Algorithmic Point of View. 2nd edition. Springer, 2016. From within USC, the book may be freely accessed at here, and supplementary material is available here.
  2. Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. Program Synthesis. Foundations and Trends in Programming Languages, 2017. Accessible from here.
  3. Michael Gordon. Background Reading on Hoare Logic. 2016. Accessible from here.
  4. Susan Horwitz. Abstract Interpretation. 2013. Accessible from here.
  5. Anders Møller and Michael Schwartzbach. Static Program Analysis. Department of Computer Science, Aarhus University. 2018. Accessible from here.

Schedule

Unit 1: Automatic Reasoning Engines

Jan 10 Course introduction, motivation, logistics.
[Slides], [Recording]
Jan 12 Propositional logic, satisfiability and validity.
[Notes], [Recording]
Jan 17 No class. Martin Luther King Jr. Day.
Jan 19 No class. Mukund at POPL.
Jan 24 Propositional logic, contd.
Jan 26 Basics of SAT solvers: DPLL and unit propagation
Jan 31 Solving Horn-SAT and 2-SAT in polynomial time.
Feb 2 Conflict-Driven Clause Learning.
Feb 7 CDCL (contd.), and introduction to Satisfiability Modulo Theories.
Feb 9 SMT: Solvers for LRA and difference logic.
Feb 14 SMT: Difference logic, DPLL(T), and theory of equality.
Feb 16 SMT: EUF and the Nelson-Oppen procedure.
Feb 21 No class. President's Day.

Unit 2: Program Synthesis

Feb 23 Introduction to program synthesis.
Feb 28 Specifying user intent with SyGuS.
Mar 2 Introduction to counter-example guided inductive synthesis (CEGIS).
Mar 7 The Enumerative SyGuS solver.
Mar 9 Stochastic and constraint-based SyGuS solvers.
Mar 14 No class. Spring Break.
Mar 16 No class. Spring Break.

Unit 3: Proof Techniques

Mar 21 The program verification problem for a simple programming language.
Mar 23 Hoare triples, weakest preconditions, and strongest postconditions.
Mar 28 Verification conditions.
Mar 30 Invariants and verifying programs with loops.
Apr 4 Proving that programs terminate.
Apr 6 Proving program termination, contd.
Apr 11 Proving program termination, contd.

Unit 4: Static Analysis and Abstract Interpretation

Apr 13 Introduction to predicate abstraction.
Apr 18 Predicate abstraction, contd.
Apr 20 Predicate abstraction, concl.

Conclusion

Apr 25 Student project presentations.
Apr 27 Course recap and research outlook.

Policies

From Dornsife's academic conduct policy: Plagiarism—presenting someone else's ideas as your own, either verbatim or recast in your own words—is a serious academic offense with serious consequences. Please familiarize yourself with the discussion of plagiarism in SCampus in Part B, Section 11, "Behavior Violating University Standards." Other forms of academic dishonesty are equally unacceptable. See additional information in SCampus and university policies on scientific misconduct, here.

Discrimination, sexual assault, intimate partner violence, stalking, and harassment are prohibited by the university. You are encouraged to report all incidents to the Office of Equity and Diversity / Title IX Office here, and / or to the Department of Public Safety. This is important for the health and safety of the whole USC community. Faculty and staff must report any information regarding an incident to the Title IX Coordinator who will provide outreach and information to the affected party. The sexual assault resource center webpage fully describes reporting options. Relationship and Sexual Violence Services webpage provides 24/7 confidential support.

Note on collaborative work: For collaborative projects, students are expected to have equal distribution of work. If there is any perceived imbalance in the collaborative project, the student should bring this to the attention of the instructor or the teaching assistant.

Assistance with writing and disabilities: Several USC's schools provide support for students who need help with scholarly writing. Check with your advisor or program staff to find out more. Students whose primary language is not English should check with the American Language Institute which sponsors courses and workshops specifically for international graduate students. The Office of Disability Services and Programs provides certification for students with disabilities and helps arrange the relevant accommodations. If an officially declared emergency makes travel to campus infeasible, USC Emergency Information will provide safety and other updates, including ways in which instruction will be continued by means of Blackboard, teleconferencing, and other technology.

Last updated: Mon Jan 24 01:41:49 PM PST 2022