# CSCI 699: Computer-Aided Verification

## Spring 2020

### Logistics

 Class: Mondays and Wednesdays, 5–6:50pm, GFS 220 Instructor: Mukund Raghothaman (raghotha@usc.edu) Office hours: Fridays, 3–5pm, or by appointment, SAL 308

### 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!

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

• April 25: Homework 3 released! Please turn it in by May 15. Two bonus questions may be found here. Please note that the bonus questions are optional: not turning them in will not negatively affect your grade.
• April 20: Sample solutions to Homework 2. For the Sudoku solver, click here.
• April 17: Ali pointed out a typo in HW2. For Question 4, instead of referring to Algorithm 4.1.1, please refer to Algorithm 4.3.1.
• Apr 4: Please use the following Zoom links for office hours today: https://usc.zoom.us/j/601134178
• Mar 21: Please use the following Zoom links for class on Monday, Mar 23, on Wednesday, Mar 25, and for office hours on Friday, Mar 27.
• Mar 21: Sample solutions to Homework 1.
• Mar 15: Homework 2 released! Please turn it in by April 8.
• Mar 9: In response to the ongoing Covid-19 pandemic, the university is temporarily moving classes to an online-only setting. See details of their announcement here. As part of this initiative, our class on Wednesday, March 11 will be delivered online through Zoom. Please use this link to attend class. I will also be available online on Friday, March 13 for office hours. Please use this link to reach me via Zoom.
• Feb 11: Nicolaas pointed out a typo in program $P_1$ of Homework 1. Please use the new version.
• Feb 5: Homework 1 released! Please turn it in by March 1.
• Jan 15: No class next week! Monday the 20th is MLK Day, and Mukund is travelling on the 22nd. See you next on Monday, Jan 27!
• Jan 13: Note project related deadlines! Submit proposal by February 19, class presentations on April 22 and April 27, and final report by May 6
• Jan 12: Course website is now live!

1. Michael Gordon. Background Reading on Hoare Logic. 2016. Accessible from here.
2. 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.
3. Anders Møller and Michael Schwartzbach. Static Program Analysis. Department of Computer Science, Aarhus University. 2018. Accessible from here.
4. Susan Horwitz. Abstract Interpretation. 2013. Accessible from here.
5. Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. Program Synthesis. Foundations and Trends in Programming Languages, 2017. Accessible from here.

### Schedule

#### Unit 1: Techniques of Proof

 Jan 13 Course introduction, motivation, logistics. [Intro slides] Jan 15 The Program Verification Problem for a Simple Programming Language. Jan 20 No class. MLK Day. Jan 23 No class. Mukund away at POPL. Jan 27 Symbolic Execution. See slides by Emina Torlak and Michael Hicks. Jan 29 Inductive invariants, verification conditions, and program correctness. See slides by Jonathan Aldrich, and Chapters 1, 2, 3 and 5 of Mike Gordon's lecture notes. Feb 3 Automatic invariant generation. See CAV 2015 tutorial presented by Madhusudan Parthasarathy and Pranav Garg. [Notes from class]. Feb 5 Proving that programs terminate. See Byron Cook et al., CACM 2011. Also see his talk on the topic.

#### Unit 2: Engines of Reason

 Feb 10 Propositional logic, satisfiability and validity. [Notes from class] Feb 13 Basics of SAT solvers: DPLL, unit propagation, and solving Horn-SAT in polynomial time. Read chapters 1 and 2 of Kroening and Strichman. [Notes from class] Feb 17 No class. President's Day. Feb 19 Solving 2-SAT in polynomial time. [Notes from class] Feb 24 Tutorial on Homework 1. [Notes from class], [Example Dafny program] Feb 26 Tutorial on Homework 1. [Notes from class] Mar 2 Conflict driven clause learning, and an introduction to SMT. See this animation of clause learning in action, and slides prepared by Clark Barrett. Read chapters 3, 4 and 10 of Kroening and Strichman. [Notes from class] Mar 4 SMT solvers (contd.) [Notes from class] Mar 9 Concluding our discussion of SMT solvers. [Notes from class]