Detecting Unrealizable Bit Vector Program Synthesis Problems

Program synthesis is the automatic construction of a computer program that adheres to a given formal specification. Contrary to traditional approaches to program construction such as compilers, program synthesis can create programs that cannot be obtained from the specification by syntactic transformations alone. This ability is essential when constructing efficient programs for specialized hardware with restricted instruction sets or when using specifications such as input-output examples. Unfortunately, the large search space of possible programs limits scalability of program synthesis in practice.
This thesis presents techniques to accelerate program synthesis of loop-free bit vector programs that are optimal with respect to a user-defined metric. Bit vector programs operate on words of data with a fixed number of bits. The presented techniques approximately decide whether a program synthesis problem is unrealizable, that is whether a collection of given operations suffices to construct a program that implements the specification. To do this, this thesis explores approaches to obtain dependencies between the input and output bits of the specification and to transfer this knowledge to the analysis of program synthesis problems. An evaluation of the presented techniques shows that they can considerably reduce the time required for the synthesis of optimal bit vector programs.
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.