S6:E4 - How Will Proof Engineering Affect the Future of Software Development
Don't just test it, prove it.
DevDiscuss · DEV
September 1, 202134m 55s
Audio is streamed directly from the publisher (dts.podtrac.com) as published in their RSS feed. Play Podcasts does not host this file. Rights-holders can request removal through the copyright & takedown page.
Show Notes
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.