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.

Schedule

Content

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.

Grading

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.

Projects

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.