S6:E4 - How Will Proof Engineering Affect the Future of Software Development

In this episode, we talk about proof engineering with Talia Ringer, researcher and incoming assistant professor at the University of Illinois at Urbana-Champaign.

Show Notes

• Scout APM (DevDiscuss) (sponsor)
• Cockroach Labs (DevDiscuss) (sponsor)
• CodeLand (sponsor)
• seL4: Formal Verification of an OS Kernel
• Formally Verified Software in the Real World
• The CompCert C Compiler
• Formal Verification of a Realistic Compiler
• Finding and Understanding Bugs in C Compilers
• QED at Large: A Survey of Engineering of Formally Verified Software
• BP: Formal Proofs, the Fine Print and Side Effects
• Proof Repair
• Talia's Ph.D. Thesis Defense: Proof Repair
• PL/FM/SE at Illinois
• Proof Repair and Code Generation
• Galois
• BedRock Systems
• How AWS’s Automated Reasoning Group helps make AWS and other Amazon products more secure
• A Solver-Aided Language for Test Input Generation
• Satnam Singh
• Silver Oak Project
• Proof Repair across Type Equivalences
• Adapting Proof Automation to Adapt Proofs
• Emily First
• RanDair Porter,
• Yuriy Brun
• Removing tokens in gallina.py
• LASER-UMASS / TacTok
• Developing Bug-Free Machine Learning Systems With Formal Mathematics
• Matthew Dwyer
• Refactoring Neural Networks for Verification
• Alex Polozov
• Evaluating Large Language Models Trained on Code

Talia Ringer

Talia Ringer is an assistant professor with the PL/FM/SE group at Illinois. She likes to build proof engineering technologies to make that world a reality. In so doing, she loves to use the whole toolbox---everything from dependent type theory to program transformations to neural proof synthesis---all in service of real humans.

Episode source