Doctoral Thesis Oral - Yi Zhou

— 5:00pm

Location:
In Person and Virtual - ET - Gates Hillman 8102 and Zoom

Speaker:
YI ZHOU , Ph.D. Candidate, 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, 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 large-scale 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 (VMware Research / University of Washington)

In Person and Zoom Participation.  See announcement.

Add event to Google
Add event to iCal