Computer Science Thesis Proposal
— 4:00pm
Location:
In Person
-
Reddy Conference Room, Gates Hillman 4405
Speaker:
YI ZHOU
,
Ph.D. Student, Computer Science Department , Carnegie Mellon University
https://yizhou7.github.io/
Towards Scalable Automated Program Verification for System Software
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, because 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 proposal, we discuss five major scalability challenges for APV: (1) memory reasoning, (2) theory reasoning, (3) reusing proofs, (4) debugging proofs, and (5) stabilizing proofs. We argue that, despite the undecidability of program verification problems in theory, we can overcome these scalability challenges in practice. Specifically, we show that there are recurrent programming and reasoning patterns in system software, which we design formal techniques to exploit. Moreover, with the help of empirical methods, we can better discover and leverage these patterns. We demonstrate that the combination of formal and empirical methods can lead to practical improvements in APV for system software.
Thesis Committee:
Bryan Parno (Chair)
Marijn Heule
Ruben Martins
Jon Howell (VMware Research / University of Washington)