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 largescale verified systems as case studies, we show this combination of formal and empirical methods leads to practical improvements in APV for system software.