CompCertSSA
 A companion web page
    CompCertSSA is built on top of the C CompCert verified compiler, by
      adding a SSA-based middle-end (conversion to SSA, SSA-based
      optimizations, destruction of SSA). This web page reports only on the
      parts of the development specific to this SSA middle-end. The complete
      development is available below.
    
    Papers
    
      -  A formally verified SSA-based middle-end. G. Barthe,
        D. Demange, and D. Pichardie. ESOP 2012.
      
 
      -  Formal Verification of an SSA-based Middle-end for
        CompCert. G. Barthe, D. Demange, and D. Pichardie. ACM TOPLAS
        2014.
      
 
      - Verifying Fast and Sparse SSA-based Optimizations in
        Coq. D. Demange, D. Pichardie and L. Stefanesco. CC 2015.
        more
      
 
      - Validating Dominator Trees for a Fast, Verified Dominance Test.
        S. Blazy, D. Demange and D. Pichardie. ITP 2015.
        more
      
 
      - Mechanizing Conventional SSA for a Verified Destruction with
        Coalescing. D. Demange and Y. Fernandez de Retana. CC 2016.
        more
      
 
      - A Fast Verified Liveness Analysis in SSA Form. JC. Léchenet,
        S. Blazy, D. Pichardie. IJCAR 2020.
        more
      
 
    
    Coq Formalization
    
      - 
        
 Project, and releases 
         Access the Gitlab project here, or
          get the latest release.
       
       CompCertSSA quick start
          
            -  Compiling CompCertSSA follows the same process as for
            CompCert (see 
            manual). 
 
            -  Usage of CompCertSSA: same as CompCert, but with
            the 
-ssa option, e.g.
	       ./ccomp -ssa on [target]  
            -  Help on CompCertSSA: same as CompCert, with 
                ./ccomp --help  
          
      
     
     Browsable version of files specific to the SSA middle-end.
         Below is a commented listing of the underlying Coq
	  specifications and proofs.  Proof scripts folded by default,
	  to unfold, click on "Proof".
        
        
	  -  The whole compilation chain, with middle-end plugged
	    in:
            Compiler
            Complements
	  
 
	  -  RTL transformations, previous to SSA generation
	    
	  
 
	  -  SSA form: definition and validation
	    
	  
 
	  -  SSA properties and libraries:
	    
	  
 
	  -  Optimizations :
	    
          
 -  CSSA form (Conventional SSA) :
            
          
 
          -  RTLpar, RTL with parallel-copy blocks:
            
          
 
          -  Deparallelization of copy-blocks, from RTLpar to RTL:
            RTLdpar
            RTLdparspec
            RTLdparproof