Exploring the Boundaries of Solvable Program Synthesis

Context and Potential Impact

Program synthesis describes the problem of generating a function (i.e. program) that satisfies a specification which is given as a logical formula. The ability of simply stating the properties a program should have (i.e. what a program should do), instead of "coding" the function by yourself (i.e. how a program should do something) has many advantages. Some of which are:

Correctness: The usual path to showing program correctness requires the writing of programs, stating of properties, and finally showing that the written program adheres to the properties specified. In program synthesis the desired properties are stated first. After that a program is constructed automatically. This resulting program is correct (i.e. adheres to the properties) by construction and therefore does not require any further steps to prove correctness.

Independence: It often occurs that one has to write duplicate code. This can happen due to a change in operating system or an underlying library. However, while all these changes may require a change in the program they do not require a change in the specification. Hence, a specification only has to be stated once and can be reused independently from the underlying system.

Efficiency: Formulating what a program should do instead of how, usually requires considerably less time. Hence, using program synthesis can speed up the development process significantly.

Even this limited set of advantages has significant impact in software development and security in general. Unfortunately, and somewhat unsurprisingly, fully fledged unrestricted program synthesis is theoretically undecidable. Hence, significant research has gone into restricting the program synthesis problem to a simpler and therefore tractable problem. One of these approaches is known as SyGuS (Syntax-guided Synthesis). SyGuS specifies a format of program synthesis problems which consists of a background theory, a syntactic restriction usually in form of a grammar, and a specification. The background theory provides the semantics for the syntax while the specification states the properties of the function which is to be synthesised. For aforementioned reasons most research is put into decidable background theories. Despite these restrictions the general SyGuS problem remains undecidable in many cases, making synthesis tools incomplete or inefficient most of the time. However, imposing further syntactic restrictions makes it possible to walk the line between the theoretically possible and impossible.

Aims, Objectives, and Novelty
In our research we seek to continue the theoretical research of what is and is not possible. By incorporating novel restrictions (in syntax and semantics) and analysing their impact on the tractability of the SyGuS problem we hope to gain a better understanding of syntax-guided synthesis and its limits. In particular, we have the following goals in mind:

Investigate the effects of syntactic sugar (e.g. ITE constructs) on the solvability of the SyGuS problem.

A more in depth analysis of SyGuS with LIA and LRA as background theories.

Describing novel classes of SyGuS problems and determining their tractability in combination with categorizing problems from pre-existing benchmark databases.

Further down the road we may look at techniques known from automated theorem proving, such as quantifier instantiation, and investigate their applications to program synthesis. Furthermore, in case one of these techniques or restrictions turns out to not only be tractable but also useful, we also intend to incorporate a procedure solving these SyGuS instances in state of the art solvers.

This project falls within the EPSRC Information and communication technologies (ICT) research area.

We plan on collaborating with Sanjit Seshia. If subsequent results turn out to have practical applications we will try to set up a collaboration with Cesare Tinelli or Armando Solar-Lezama.