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.. |
BibTeX: |
@article{Minimal_SSA-AFP,
author = {Max Wagner and Denis Lohner},
title = {Minimal Static Single Assignment Form},
journal = {Archive of Formal Proofs},
month = jan,
year = 2017,
note = {\url{http://isa-afp.org/entries/Minimal_SSA.html},
Formal proof development},
ISSN = {2150-914x},
}
|