Section: New Software and Platforms

CompcertSSA

Keywords: Optimizing compiler - Formal methods - Proof assistant - SSA

Functional Description: CompcertSSA is built on top of the Compcert verified C compiler, by adding a middle-end based on the SSA form (Static Single Assignment) : conversion to SSA, SSA-based optimizations, and destruction of SSA.

• Participants: Sandrine Blazy, Delphine Demange, Yon Fernandez de Retana, David Pichardie and Leo Stefanesco

• Contact: Delphine Demange

• Publications: Mechanizing conventional SSA for a verified destruction with coalescing - Validating Dominator Trees for a Fast, Verified Dominance Test - A Formally Verified SSA-based Middle-end : Static Single Assignment meets CompCert - Formal Verification of an SSA-based Middle-end for CompCert - Verifying Fast and Sparse SSA-based Optimizations in Coq.

• URL: http://compcertssa.gforge.inria.fr/