Validating Dominator Trees for a Fast, Verified Dominance Test
Proofs and experiments

Submitted paper


Source code

Download the Coq development and browse our experiments' results (please wait while loading).

Main files


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.

  1. Unzip the archive
  2. Compile compcertSSA
    	  cd compcertSSA_itp15
    	  ./configure ia32-macosx 
    	  make all
    	  cd compcertSSA_itp15
    	  ./configure ia32-linux
    	  make all
  3. Run experiments (after having compiled compcertSSA)
    	  cd compcertSSA_itp15 (if necessary)
    	  make dom_benchs
    then read benchs/bench_dom.html with a web browser.