Verifying Fast and Sparse SSA-based Optimizations in Coq. Delphine Demange, David Pichardie, Léo Stefanesco. CC 2015.
Download the Coq development and browse our experiments' results (please wait while loading).
To get the latest stable release of the compiler (with a commented, browsable version of proofs), go to the main web page of the project.
As indicated on the paper, all tests were done on a MacBook OSX 10.8.5, 2.9GHz Intel Core i7, 8GB 1600MHz DDR3.
The version of Coq used in this work is version version 8.4pl2 (January 2014) compiled on Jan 28 2014 10:19:40 with OCaml 4.01.0.
Experiments have been made with the x86 back-end, on Mac OSX (otherwise, experimental results might slightly differ).
cd compcertSSA_cc15 ./configure ia32-macosx make depend make -j2 all
cd compcertSSA_cc15 (if necessary) cd test ./run_benchs.shthen open compcertSSA_cc15/bench.html in your web browser.