Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP article: Verified Construction of Stat...

view this post on Zulip Email Gateway (Aug 22 2022 at 12:51):

From: Tobias Nipkow <nipkow@in.tum.de>
Verified Construction of Static Single Assignment Form
Sebastian Ullrich, Denis Lohner

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.

http://afp.sourceforge.net/entries/Formal_SSA.shtml

Enjoy!
smime.p7s

Last updated: Nov 21 2024 at 12:39 UTC