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 my work on proof repair, a proof engineering technology that makes it easier to maintain or redesign pieces of verified systems. My work on proof repair uses a combination of semantic differencing, a configurable proof term transformation, and a proof term to tactic decompiler to adapt proofs to breaking changes in type definitions. The proof term transformation implements transport across certain equivalences in a way that is suitable for repair and does not rely on axioms beyond those Coq assumes. This is implemented in a flexible proof repair tool that has been used to support proof engineering benchmarks, ease development with dependent types, and support an industrial proof engineer to more easily interoperate between Coq and other verification tools.
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.
Attend this talk by clicking here.
A password is required to enter this Zoom event. If you need this password, please see the event announcements on the college email lists or contact Alex Taubman.