Proof Engineering Tools for a New Era

September 30, 2021
3:00 - 4:00 pm ET
Halligan 102,or Zoom
Speaker: Talia Ringer, University of Illinois CS
Host: Dan Votipka

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 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.

Speaker will make presentation via Zoom. Halligan 102 or Zoom are both available.

Join Zoom Meeting: https://tufts.zoom.us/j/97183120811

Meeting ID: 971 8312 0811

Password: See colloquium email

Dial by your location: +1 646 558 8656 US (New York)

Meeting ID: 971 8312 0811

Passcode: See colloquium email