Proof Repair
30/11/2021, 9am
Speaker
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 using interactive theorem provers. Still, the costs of developing these verified systems are high, and the costs of maintaining them even higher. These costs are addressed by proof engineering: technologies thatmake it easier to develop and maintain verified systems.
This talk will present some of the key challenges that proof engineering addresses, focusing in particular on my work on proof repair. In contrast with traditional proof automation, proof repair views proofs as fluid entities that must evolve alongside the programs whose correctness they prove. My work onproof repair uses a combination of semantic differencing and program transformations on proof terms to adapt proofs to breaking changes. I have implemented these techniques in a flexible proof repair tool called PUMPKIN PATCH. PUMPKIN PATCH has already been used to support proof engineering benchmarks, ease development with dependent types, and simplify a mechanizedverification of the TLS Handshake protocol.
Speaker Bio
Talia Ringer is an Assistant Professor at the University of Illinois at Urbana-Champaign. Her work makes it easier for proof engineers to develop and maintain verified systems. She finished her Ph.D. in computer science from the University of Washington in June 2021. Before graduate school, she worked as a software engineer at Amazon for three years. She is founder and chair of the SIGPLAN Long-Term Mentoring Committee ,and is active in diversity, service, and outreach.