Mechanizing Conventional SSA for
a Verified Destruction with Coalescing

Paper

Mechanizing Conventional SSA for a Verified Destruction with Coalescing. D. Demange and Y. Fernandez de Retana. CC'16. preprint pdf

Source code

Download the Coq development

Main files

Experiments

The version of Coq used in this work is version 8.4pl6 (April 2015) compiled with OCaml 4.02.2.

  1. Unzip the archive
  2. Compile compcertSSA
              cd coalescing
              ./configure ia32-linux  # or ia32-macosx, etc...
              make depend
              make all
  3. Run experiments (after having compiled compcertSSA)
              cd test (if necessary)
              make coalescing
              make spilling
    Then each subfolder of "test" will contain files with results named results_coalescing.out and results_spilling.out for each test.