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
DevNews (sponsor)
CodeNewbie (sponsor)
DataStax (sponsor)
Cockroach Labs (DevDiscuss) (sponsor)
Swimm (DevDiscuss) (sponsor)
Stellar (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.