Bachelorarbeit (abgeschlossen)

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.

Zusätzlich soll eine Transformation eines Steuerflussgraphen in SSA-Form (axiomatisch) definiert werden und dessen Korrektheit bezüglich der in dieser Arbeit entworfenen SSA-Definition gezeigt werden.

Aufgabe

• Erarbeiten einer axiomatischen SSA-Definition in Isabelle/HOL
• Entwurf und Verifikation einer Transformation nach 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

Verified Construction of SSA Form

Betreuer

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

Studenten

Ehemalige Mitarbeiter
Dr.-Ing. Sebastian Ullrich