HOME | ENGLISH | IMPRESSUM | KIT

Bachelorarbeit (abgeschlossen): Formalisierung von SSA-Form

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.

'If-Diamant' in SSA-Form

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

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

Wissenschaftliche Mitarbeiter
Sebastian Buchwald
Denis Lohner

Studenten

Wissenschaftliche Mitarbeiter
Sebastian Ullrich