Moderne Compiler-Zwischensprachen nutzen SSA-Form um Analysen und Optimierungen zu vereinfachen. SSA-Form verlangt, dass jeder Verwendung einer Variable genau eine Definitionsstelle zugeordnet werden kann. Um dies zu erreichen, werden sogenannte ϕ-Funktionen eingeführt, die abhängig vom Programmablauf verschiedene Definitionen auswählen.

Kontext dieser Arbeit ist die Konstruktion von SSA-Form. Es soll untersucht werden welche (zusätzlichen) Eigenschaften direkt nach dem SSA-Aufbau gelten. Anhand dieser Eigenschaften soll eine axiomatische SSA-Definition in Isabelle/HOL erarbeitet werden.

Zur Evaluierung der Axiomatisierung soll ein einfaches Kriterium für die Konstruktion minimaler SSA-Form verifiziert werden.

Aufgabe

• Erarbeiten einer axiomatischen SSA-Definition in Isabelle/HOL
• Verifikation eines Kriteriums für die Konstruktion minimaler SSA-Form

Literatur

• Einführung in Isabelle/HOL: Tutorial und Praktikum
• Cytron et al.: Efficiently computing static single assignment form and the control dependence graph

Voraussetzungen

• Gute Fertigkeiten im mathematischen Beweisen
• Freude an formal korrektem Arbeiten
• Kenntnisse in funktionaler Programmierung sind vorteilhaft, aber nicht notwendig
• Grundkenntnisse im Compilerbau sind vorteilhaft, aber nicht notwendig



Veröffentlichungen

Veröffentlichung

Minimal Static Single Assignment Form

Betreuer

Ehemalige Mitarbeiter
Dipl.-Inform. Sebastian Buchwald
Dipl.-Inform. Denis Lohner

Studenten

Ehemalige Mitarbeiter
M.Sc. Maximilian Wagner