Proof Engineering Tools for a New Era
Abstract: Interactive theorem provers make it possible to prove that a program satisfies a specification. This provides a high degree of certainty that the program is trustworthy. The last two decades have marked a new era of verification of large and critical systems, including operating system kernels, machine learning systems, compilers, and distributed systems. Proving correct deployable software of this scale has introduced engineering challenges beyond those seen either in traditional software engineering or in traditional small-scale formal proof. These challenges are addressed by proof engineering--technologies that make it easier to develop and maintain verified systems.
This talk will present some of the challenges that proof engineering addresses. It will focus on my work on proof repair, which extends traditional proof automation to address the challenges of maintaining or redesigning pieces of verified systems. My work on proof repair uses a combination of semantic differencing and program transformations on proof terms to adapt proofs to breaking changes. In contrast with traditional proof automation, proof repair views proofs as fluid entities that must evolve alongside the programs whose correctness they prove. It aims to empower proof engineers to not only develop but also maintain verified systems, a challenge that is particularly salient in this new era of verification at scale.
Bio: Talia Ringer is a PhD candidate in programming languages at University of Washington. Her main interest is in making program verification using interactive theorem provers more accessible through better proof engineering tools and practices, especially when it comes to maintaining proofs as programs change over time. Her vision is a future of verification that is accessible to all programmers, not just to experts. She believes that this will help make software more reliable and secure. In addition to her own contributions to this end, she has authored a 120-page survey of proof engineering. Prior to graduate school, she earned her bachelor's in mathematics and computer science from University of Maryland, then worked at Amazon as a software engineer for three years. She is an NSF GRFP fellow and a contributor to the Coq interactive theorem prover. She is active in advising, mentorship, service, and outreach.
A pizza lunch for attendees will be available at 11:45 a.m. in CS 150