Pete's Footprints
summary
Thirty years of follow-on work traces specific technical moves: an effect system in a Standard ML compiler used to prove correctness of optimizations, relational logical-relations handling dynamically allocated store, a relational form of separation logic pushed down to machine code with a Coq-extracted bootable image, mechanized proofs of an allocator and of high-level types over x86, use of Iris separation logic to verify microkernel code at Meta, and deployment toward Infer / incorrectness logic on 100 million lines of Hack.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:25Early interest in linear logic
- 2:30Bunched implications challenge
- 3:35Effect systems and optimizations
- 4:39Separation logic revolutionizes reasoning
- 6:28Parametricity and mutable storage
- 8:53Understanding logical relations
- 10:38Revisiting separation logic foundations
- 12:23Applying techniques to low-level languages
- 13:51Verifying machine code
- 14:31Facebook's Infer and Incorrectness Logic
- 15:58Challenges of under-approximation
- 16:21Q&A
related talks
57mInvited Talk: Bridging Safety and Performance
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
21mMechanised Hypersafety Proofs about Structured Data
01h 05mVerifying Infinitely Many Programs at Once
52mThink Abstractly, Work Concretely
23mSpecifying and Verifying Future Conditions
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...