Yi Zhou

Towards Scalable Automated Program Verification for System Software Degree Type: CS
Advisor(s): Bryan Parno
Graduated: May 2025

Abstract:

Automated Program Verification (APV) provides formal guarantees about
software while promising strong automation in the verification process. APV has
already seen preliminary successes in system software (e.g., file systems, network
protocols), extending beyond academic prototypes to industrial applications.
However, the scalability of APV becomes an issue as we move towards more
complex systems, where automation failures start to show up. Such failures
often require tedious manual fixes, breaking the pledge of automation in APV.
Worse yet, since program verification is fundamentally undecidable, automation
failures are inherently inevitable.
Nevertheless, that does not mean APV is hopeless beyond small-scale systems.
In this thesis, we organize the discussion around the development stages of APV:
(1) creating proofs, (2) reusing proofs, (3) debugging proofs, and (4) stabilizing
proofs. We argue that, despite the undecidable nature of program verification
in theory, we can overcome the scalability challenges that arise in practice, due
to the recurrent patterns in APV programming and reasoning.
Specifically, we make empirical observations on the common motifs in APV,
and then design formal methods to leverage them for automation. Using largescale
verified systems as case studies, we show this combination of formal and
empirical methods leads to practical improvements in APV for system software.

Thesis Committee:
Bryan Parno (Chair)
Marijn Heule
Ruben Martins
Jon Howell (University of Washington)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Keywords:
Program Verification, System Software, First-Order Logic, Satisfiability Modulo Theories