HOME | ENGLISH | IMPRESSUM | KIT

Bachelorarbeit (offen): Survey Programmsynthese

Die Aufgabe von Programmsynthesealgorithmen ist es, aus einer Spezifikation ein optimales Programm zu konstruieren. Diese Spezifikation kann eine logische Beschreibung des gewünschten Programmverhaltens sein, oder ein bestehendes, aber nicht optimales Programm. Im letzteren Fall spricht man von Superoptimierung. In unserer Arbeitsgruppe arbeiten wir an Anwendungen dieser Techniken im Compilerbau [1, 2].

Durch mehr verfügbare Rechenleistung und Fortschritte bei SAT-/SMT-Solvern gab es zum Thema Programmsynthese und Superoptimierung in letzter Zeit wieder viel Fortschritt. Sie sollen uns in dieser Arbeit einen fundierten Überblick über den Stand der Technik geben und die vorhandenen Tools bewerten.

Aufgabe:

  • Vergleich der vorhandenen Ansätze
  • Definieren einer Benchmark-Suite
  • Evaluation der Tools anhand Ihrer Benchmarks

Voraussetzungen

  • Spaß an Literaturrecherche
  • Kenntnisse in SAT/SMT-Solving vorteilhaft
  • Leidenschaft für saubere wissenschaftliche Experimente
  • Die Fähigkeit, wissenschaftliche Prototypen zum Laufen zu bringen

Schlüsselworte

Compiler, SMT, Synthese 

Betreuer

Wissenschaftliche Mitarbeiter
Sebastian Buchwald
Andreas Fried