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 that make 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 on proof 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 mechanized verification of the TLS Handshake protocol.
Bio:
Talia Ringer is a PhD candidate at the Paul G. Allen School of Computer Science & Engineering at the University of Washington. Her work makes it easier for proof engineers to maintain verified systems. 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.
Faculty host: Grigore Rosu
