Verified Software at Scale
summary
Mechanized WebAssembly semantics now feed the standard, with a formal DSL that produces parser tests, reference interpreters and automatically generated semantics from a Wasm DSL, and a machine-checked proof that proved type-safe module instantiation for Wasm. Tools like Gillian expose a language-independent, axiomatic interface for function-level symbolic execution enabling Gillian-based compositional symbolic execution and incorrectness proofs, experiments linking optimized interpreter code to proof logs, and an AWS message-deserialization verification that compiles and runs.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 3:04Theory to practical verification
- 7:44WebAssembly formal semantics
- 11:43Compositional verification
- 19:13Parametric verification with Gillian
- 21:05Verifying AWS code
- 23:14Concurrent verification
- 26:47Complexity in verification
- 27:57Closing remarks
- 28:19Q&A
related talks
43mGillian: a Multi-language Platform for Compositional Symbolic Analysis
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
34mWasm Components: The Interchangeable Parts of Software
32mCorrectness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
22mCreate an Extensible Cloud Native Application with WebAssembly
40mFormal semantics for multi-language programs
01h 02mLanguage Design meets Verifying Compilers
21mMOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs