Aarhus University Seal / Aarhus Universitets segl

Special talk by Talia Ringer on Proof Engineering Tools for a New Era

15.02.2021 | Søs Küster Markussen

Date Mon 01 Mar
Time 17:00 18:00
Location Online - Zoom meeting

Special talk by Talia Ringer on 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 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.

CS frontpage, Featured, Public/media