### Abstract

We define a functional variant of the static single assignment (SSA) form construction algorithm described by Braun et al., which combines simplicity and efficiency. The definition is based on a general, abstract control flow graph representation using Isabelle locales.

We prove that the algorithm's output is semantically equivalent to the input according to a small-step semantics, and that it is in minimal SSA form for the common special case of reducible inputs. We then show the satisfiability of the locale assumptions by giving instantiations for a simple While language.

Furthermore, we use a generic instantiation based on typedefs in order to extract OCaml code and replace the unverified SSA construction algorithm of the CompCertSSA project with it.

A more detailed description of the verified SSA construction can be found in the paper Verified Construction of Static Single Assignment Form, CC 2016.

### License

BSD License

### Topics

- Computer science/Programming languages/Compiling

### Session Formal_SSA

- FormalSSA_Misc
- Serial_Rel
- Mapping_Exts
- RBT_Mapping_Exts
- Graph_path
- SSA_CFG
- Minimality
- Construct_SSA
- Construct_SSA_notriv
- SSA_Semantics
- While_Combinator_Exts
- SSA_CFG_code
- Construct_SSA_code
- SSA_Transfer_Rules
- Construct_SSA_notriv_code
- Generic_Interpretation
- Generic_Extract
- Disjoin_Transform
- WhileGraphSSA

### Depends on

- The CAVA Automata Library
- Collections Framework
- Dijkstra’s Shortest Path Algorithm
- Towards Certified Slicing

### Used by

- Minimal Static Single Assignment Form

### Auto-related entries

- Minimal Static Single Assignment Form

## Cite

×

Formal_SSA-AFP

    @article{Formal_SSA-AFP,
      author  = {Sebastian Ullrich and Denis Lohner},
      title   = {Verified Construction of Static Single Assignment Form},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Formal_SSA.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- Feb 8, 2016 : Isabelle2015