Discover_degrade_bg_blanc.png

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.

Last Updated 2018-03-13 Tue 16:39