Validating Dominator Trees for a Fast, Verified Dominance Test. S. Blazy, D. Demange and D. Pichardie. ITP 2015. [.pdf].
Download the corresponding Coq development snapshot.
Browse our experiments' results (please wait while loading).
CompCertSSA main web page.
As indicated on the paper, all tests were done on a MacBook OSX 10.8.5, 2.3GHz Intel Core i7, 8GB 1600MHz DDR3 memory.
The version of Coq used in this work is version 8.4pl2 (June 2013) compiled with OCaml 4.01.0.
cd compcertSSA_itp15 ./configure ia32-macosx make allor
cd compcertSSA_itp15 ./configure ia32-linux make all
cd compcertSSA_itp15 (if necessary) make dom_benchsthen read benchs/bench_dom.html with a web browser.