CS 6110 Software Verification

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!



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

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

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

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


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.