body
Code and other tools
- CompCertSSA : built on top of the C CompCert verified compiler, by adding a SSA-based middle-end (conversion to SSA, SSA-based optimizations, destruction of SSA).
- Verified Concurrent Garbage Collector : a Rely/Guarantee proof methodology applied to the verification of an on-the-fly concurrent garbage collector.
- Rely-Guarantee logic for Simple Linearizability : a Rely/Guarantee program logic and its use for proving semantic refinement about linearizable data structures.
- Sea of Nodes : a first semantic account of the Sea of Nodes compiler intermediate representation. Available Coq formalization.