An Iris Instance for Verifying CompCert C Programs
summary
Rebuilds VST’s program logic inside Iris to verify C as defined by CompCert, providing an Iris instance of CompCert C with a custom shared-value algebra that models CompCert permissions (readable/writable/non-empty). Implements new weakest-precondition/Hoare-triple definitions, recreates the Floyd tactic library, and runs the full VST example suite successfully; proofs shrink by about 43% proof-size reduction while preserving CompCert-level adequacy and executable guarantees.
AI-written summary · about
chapters (8)
- 0:00Separation logic session intro
- 0:42Iris framework overview
- 3:28ComCERT memory model changes
- 6:19Shared values resource algebra
- 9:28Logical ownership to ComCERT
- 10:54Rebuilding VST in Iris
- 12:40Future plans and implications
- 13:24Q&A
related talks
22mDestabilizing Iris
01h 06mVerifying a compiler through equational means
01h 03mCRIS: The power of imagination in specification and verification- 01h 06mVerifying a compiler through equational means
18mWP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
20mA Verified Foreign Function Interface Between Coq and C
21mThe New Verification Ecosystem that Supports RISC-V Verification fo...