Detecting Unrealizable Bit Vector Program Synthesis Problems

Description

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.