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
| Ehemalige Mitarbeiter |
|---|
| M.Sc. Andreas Fried |