Foundational Integration Verification of Diverse Software and Hardware Components | MIT CSAIL
csail.mit.edu · 477 words · saved by 1 readers
Massachusetts Institute of Technology Computer Science & Artificial Intelligence Laboratory 32 Vassar St, Cambridge MA 02139
Back to Events Foundational Integration Verification of Diverse Software and Hardware Components Speaker Andres Erbsen MIT CSAIL December 19 2022 12:00 P - 2:30 P Location Seminar Room G882 (Hewlett Room) Abstract: The engineering of computer systems is distinguished by a long-standing tradition of building on quicksand. Even the most venerable and critical systems have a history of serious bugs and security vulnerabilities. Human fallibility continues to prevail. Computer-checked mathematical proofs of software correctness have emerged as a promising method to rule out large classes of bugs.
related reading
- A shallow dive into formal verificationvitalik.eth.limo
- When AI Writes the World's Software, Who Verifies It? — Leonardo de Mouraleodemoura.github.io
- Computers can be understood - Made of Bugsblog.nelhage.com
- MIT 6.512, Fall 2025frap.csail.mit.edu
- Software Foundationssoftwarefoundations.cis.upenn.edu
- Formally Verifying the Easy Partbrainflow.substack.com
- What the Proofs Assume | seL4sel4.systems
- The Case Against Formal Verification, 50 Years Laterivan-gavran.github.io
- Broken proofs and broken proverslawrencecpaulson.github.io
- The Compute Verification Postfirstscattering.com
- lf-lean: The frontier of verified software engineering | Theoremtheorem.dev
- The Shape of the Systemshapeofthesystem.com