Detecting Unrealizable Bit Vector Program Synthesis Problems

Beschreibung

Programmsynthese ist die automatische Konstruktion eines Computerprogramms, das eine gegebene formale Spezifikation erfüllt. Anders als herkömmliche Verfahren zur Programmkonstruktion wie Übersetzer, kann Programmsynthese Programme erzeugen, die nicht nur durch rein syntaktische Transformationen aus der Spezifikation abgeleitet werden können. Diese Fähigkeit ist essenziell für die Erzeugung effizienter Programme für spezialisierte Hardware mit eingeschränktem Instruktionssatz oder um Spezifikationen wie Eingabe-Ausgabe-Beispiele nutzen zu können. Leider begrenzt der große Suchraum möglicher Programme die Skalierbarkeit der Programmsynthese in der Praxis. Diese Dissertation stellt Techniken vor, um die Programmsynthese schleifenfreier Bitvektor-Programme, die für eine nutzerdefinierte Metrik optimal sind, zu beschleunigen. Bitvektor-Programme verarbeiten Daten fester Bitbreite. Die vorgestellten Techniken stellen approximativ fest, ob ein Programmsyntheseproblem unlösbar ist, das heißt, ob die gegebenen Operationen ausreichen, um daraus ein Programm zu konstruieren, das die Spezifikation implementiert. Dazu untersucht diese Dissertation Ansätze, um die Abhängigkeiten zwischen Eingabe- und Ausgabe-Bits der Spezifikation zu bestimmen und dieses Wissen für die Analyse von Programmsyntheseproblemen einzusetzen. Eine Auswertung der vorgestellten Techniken zeigt, dass sie die notwendige Zeit zur Synthese optimaler Bitvektor-Programme deutlich reduzieren können.