Email Gateway (Aug 22 2022 at 14:58): Email Gateway (Aug 22 2022 at 14:58):From: Tobias Nipkow <nipkow@in.tum.de>
Minimal Static Single Assignment Form
Max Wagner and Denis Lohner
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..
https://www.isa-afp.org/entries/Minimal_SSA.shtml
Enjoy!
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC