Skip to main content
Open Access Publications from the University of California

UC San Diego

UC San Diego Electronic Theses and Dissertations bannerUC San Diego

Reducing the Costs of Proof Assistant Based Formal Verification or : Conviction without the Burden of Proof


This thesis considers the challenge of fully formal software verification in the demanding and foundational context of mechanical proof assistants. While this approach offers the strongest guarantees for software correctness, it has traditionally imposed tremendous costs to manually construct proofs. In this work, I explore techniques to mitigate this proof burden through careful system design. In particular, I demonstrate how formal shim verification and extensible compiler techniques can radically reduce the proof burden for realistic implementations of critical modern infrastructure

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View