S6:E4 - How Will Proof Engineering Affect the Future of Software Development
09/01/21 • 34 min
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 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.
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 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.
Previous Episode
S6:E3 - What Makes Ethical Design in Your Product and Your Company
In this episode, we talk about what makes ethical design in your product and your company with Sarah Fossheim, creator of the Ethical Design Guide, and Aubrey Blanche, director of equitable design at Culture Amp.
Show Notes- DevNews (sponsor)
- CodeNewbie (sponsor)
- DataStax (sponsor)
- Cockroach Labs (DevDiscuss) (sponsor)
- Swimm (DevDiscuss) (sponsor)
- Stellar (sponsor)
- Ethical Design Guide
- Culture Amp
- Want to Read Rate this book 1 of 5 stars2 of 5 stars3 of 5 stars4 of 5 stars5 of 5 stars Open Preview Weapons of Math Destruction: How Big Data Increases Inequality and Threatens Democracy
Sarah Fossheim is a multidisciplinary developer, designer and accessibility specialist. They have a strong focus on dataviz accessibility and usability. Currently Sarah is working as an independent consultant, educator and advisor, helping companies create more accessible and inclusive solutions.
Aubrey BlancheAubrey Blanche is The Mathpath (Math Nerd + Empath), Director of Equitable Design & Impact at Culture Amp, and a startup investor, and advisor. She questions, reimagines, and redesigns the systems that surround us to ensure that all people access equitable opportunities.
Next Episode
S6:E5 - When You Should Start Thinking About Performance
In this episode, we talk about web performance with Todd Underwood, senior director of engineering and SRE at Google.
Show Notes- DevNews (sponsor)
- CodeNewbie (sponsor)
- DataStax (sponsor)
- Cockroach Labs (DevDiscuss) (sponsor)
- Swimm (DevDiscuss) (sponsor)
- Stellar (sponsor)
Todd Underwood is a director at Google. He leads machine learning for site reliability engineering (SRE) for Google. ML SRE teams build and scale internal and external ML services and are critical to almost every product area at Google. He is also the engineering site lead for Google’s Pittsburgh office.
If you like this episode you’ll love
Episode Comments
Generate a badge
Get a badge for your website that links back to this episode
<a href="https://goodpods.com/podcasts/devdiscuss-175374/s6e4-how-will-proof-engineering-affect-the-future-of-software-developm-16366969"> <img src="https://storage.googleapis.com/goodpods-images-bucket/badges/generic-badge-1.svg" alt="listen to s6:e4 - how will proof engineering affect the future of software development on goodpods" style="width: 225px" /> </a>
Copy