**Instructor:** Pavel Panchekha 〈pavpan@cs.utah.edu〉

**TA**: Manasij Mukherjee 〈manasij@cs.utah.edu〉

**Textbook:** The Calculus of Computation, 2007

**Office Hours:** After class or individually scheduled in *MEB 2174*

This course teaches the foundations of software verification: of analyzing complex software to find or excise bugs. It will cover logic and decision procedures; symbolic execution and program logics; and abstract interpretation and dependent types. Homework assignments based on popular verification and analysis tools will provide hands-on experience, while research papers will introduce the state of the art.

Organization will be on Canvas. Discussion will be on Piazza. Lecture will be on Zoom.

Please fill out course evals!

*Part 1: Automated Reasoning***7 Jan***Course Introduction*

Why verify, Course info, How to verify

Slides (PDF), Feedback**9 Jan***Propositional Logic*

Semantics, Resolution, and DPLL

Chapter 1, Slides (PDF), Feedback

Further Reading on Clausal Learning**14 Jan***First-order Logic*

Syntax, Semantics, and Theories

Chapter 2, Slides (PDF), Feedback**16 Jan***Proofs and Deduction*

Proofs, Axioms, and Completeness

LogiText, Slides (PDF), Feedback

MiniSat assignment due**21 Jan***First-order Theories*

Chapter 3, Slides (PDF, demo), Feedback

Equality, Arithmetic, Arrays**23 Jan***The Nelson-Oppen Mechanism*

Chapter 10, Slides (PDF), Feedback

Isolation by theory, SMT solvers, SMT-LIB**28 Jan***Equality Saturation*

Chapter 9, Slides (PDF), Feedback

Hashing, equivalence classes, pattern matching**30 Jan***Linear Arithmetic*

Chapter 8, Slides (PDF), Feedback

More: Fourier-Motzkin, Omega Test

Linear equalities, variable elimination, complexity

Z3 assignment due**4 Feb***Theory of Arrays*

Chapter 11, Slides (PDF), Feedback

Read-over-write, array equalities, array properties**6 Feb***Decision Procedures for Web Accessibility*

Paper, Slides (PDF),

Web layout, finitization, modularity

Project Proposals due

*Part 2: Reasoning about Programs***11 Feb***Programming Language Semantics*

Guest lecture by*Matthew Flatt*

Notes

Substitution, reduction, evaluation**13 Feb***Symbolic Evaluation*

Original Sources, Slides (PDF), Feedback

Environments, path conditions, feasiblity**18 Feb**Project Proposal Presentations**20 Feb***Hoare Logic*

Axioms, weakest preconditions

Chapter 5.1, Slides (PDF), Feedback

KLEE assignment due**25 Feb***Semantics of Loops*

Invariants, termination

Chapter 5.2.1, Slides (PDF, demo), Feedback**27 Feb***Semantics of Procedures*

Pre-/post-conditions, separation

Chapter 5, Slides (PDF, demo), Feedback**3 Mar**Project Milestone I Presentations**5 Mar***Verification with Transition Systems*

Guest lecture by*James Wilcox*

Mypyvy, Slides (PDF)

Dafny and Mypyvy demos

Dafny assignment due**10 Mar**No class: Spring Break**12 Mar**No class: Spring Break

*Part 3: Static Analysis***17 Mar**Optional video lecturing debugging**19 Mar***Abstract Interpretation*

Lecture, Slides (PDF), Feedback**24 Mar***Common Domains*

Lecture, Slides (PDF, demo), Feedback**26 Mar**Project Milestone II Presentations**31 Mar***Demo: Checker Framework*

Lecture, Demo Code, Feedback**2 Apr***Demo: Lean*

Lecture, Demo Code, Feedback**7 Apr***Curry-Howard Isomorphism*

Lecture, Slides (PDF, demo), Feedback**9 Apr***Inductive Types*

Lecture, Slides (PDF, demo), Feedback**14 Apr***Type Dependency*

Lecture, Slides (PDF, demo), Feedback**16 Apr***Fast Correct Crypto*

Reading, BoringSSL

Lecture, Slides (PDF, demo), Feedback

Final Project Presentations**21 Apr***Course Conclusion*

Lecture, Slides (PDF), Course Eval

Final Project Questions & Code**23 Apr**Final Project Answers

This course comes in three parts: automated reasoning, program analysis, and static analysis.

Automated reasoning means stating what the program should do. It includes:

- Logic: how we state facts about programs, infer facts from other facts, and prove or disprove them.
- Decision Procedures: how we algorithmically decide the truth or falsity of logical statements.

Program analysis means determining what the program actually does. It includes:

- Symbolic Execution: how we reason about program expressions, branches, and functions.
- Program Logic: how we reason about imperative programs, subroutines, and loops.

Static analysis scales the prior material to large programs. It includes:

- Abstract Interpretation: how coarser-grained reasoning scales program logic to larger programs.
- Dependent Types: how finer-grained reasoning scales program logic to larger programs.

Your grade will be 50% project, 10% participation, and 10% for each assignment. The project grade is 5% proposal, 5% for each of the proposal, milestone I, and milestone II presentations, 20% for the final presentation (10% your presentation, 5% your questions on others’ presentations, and 5% your answers to questions) and 10% for results. The participation grade is 5% attendance (automatic after Spring Break due to the coronavirus) and 5% feedback every class.

Late assignments must be discussed with instructor 48 hours in advance, or will be penalized 20 points.

The course project ought to either develop a verified program or a verification tool. Verification is difficult! I don’t expect every project to succeed at its goal. That said, ambition is important! I expect projects to propose challenging goals.