University of Washington
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.
The focus of my dissertation is proof engineering technologies that make it easier to develop and maintain verified systems using interactive theorem provers with an emphasis on maintenance. These technologies have in recent years helped proof engineers verify large and critical systems. When it comes to maintaining these systems, however, proof engineering is decades behind software engineering. Existing proof maintenance techniques cannot handle changes that occur outside of the proof engineer’s control, a challenge that may become more salient as verified systems continue to grow in scale. To address this, my dissertation introduces proof repair: a new generation of proof automation that adapts 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. Proof repair aims to empower proof engineers to not only develop but also maintain verified systems.