CompCert: a journey through the landscape of mechanized semantics for verified co...
summary
CompCert implements 18 verified compiler passes across 11 formally‑specified languages and proves semantics preservation by composable small-step semantics and simulation diagrams; the semantics use continuations to avoid rule-generated instructions and an anti‑stuttering measure to handle divergence. The constant‑time extension adds leak events to traces and proves preservation via leakage-erasing simulations that allow erased leak steps when erasure decisions are public. A verified JIT uses nested simulations to relate evolving programs, and a reusable memory‑model and simulation libraries support these proofs.
AI-written summary · about
chapters (6)
- 0:00Introduction to CompCert
- 5:30Scaling to real compilers
- 18:24Cryptographic constant time
- 31:05Verifying JIT compilation
- 37:01Reusability and conclusion
- 39:47Q&A session
related talks
28mMemory simulations, security and optimization in a verified compiler
15mMy Journey in Secure Compilation
20mVerified Density Compilation for a Probabilistic Programming Language
19mFormally Verifying Optimizations with Block Simulations
01h 05mMuch Still to Do in Compiler Verification (A Perspective from the CakeML Project)
15mCompiling with Continuations, Correctly
23mCorrect Compilation of Concurrent C Code
26mCombining Small-Step and Big-Step Semantics to Verify Loop Optimizations