### Abstract

This formalization is an extension to "Verified Construction of Static Single Assignment Form". In their work, the authors have shown that Braun et al.'s static single assignment (SSA) construction algorithm produces minimal SSA form for input programs with a reducible control flow graph (CFG). However Braun et al. also proposed an extension to their algorithm that they claim produces minimal SSA form even for irreducible CFGs.
In this formalization we support that claim by giving a mechanized proof.

As the extension of Braun et al.'s algorithm aims for removing so-called redundant strongly connected components of phi functions, we show that this suffices to guarantee minimality according to Cytron et al..

### License

BSD License

### Topics

- Computer science/Programming languages/Compiling

### Session Minimal_SSA

- Irreducible

### Depends on

- Verified Construction of Static Single Assignment Form

### Auto-related entries

- Formalizing the Logic-Automaton Connection

## Cite

×

Minimal_SSA-AFP

    @article{Minimal_SSA-AFP,
      author  = {Max Wagner and Denis Lohner},
      title   = {Minimal Static Single Assignment Form},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Minimal_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 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Jan 19, 2017 : Isabelle2016-1