Inductive synthesis theories and algorithms

Research has been active in the area ``inductive" program synthesis. Inductive approaches tend to iteratively compute programs by observing a few examples of expected input-output behaviour. Many state-of-the-art inductive program synthesis techniques are based on two main components: a verifier and a synthesiser. The synthesiser generates a candidate program, whilst a verifier (a human or another program) checks if the candidate meets the high-level description. If so, then a correct program is found. Otherwise, the verifier provides the synthesiser with an example demonstrating why the candidate program is incorrect. The synthesiser then attempts to find an alternative program guided by the example provided. This process continues until a correct program is found. Whether a solution is reached is determined by several factors including the correctness of the high-level description and the choice of examples provided to the synthesiser.
However, in practice, high-level descriptions tend to be partial and sometimes incorrect, thus causing existing synthesis algorithms to fail. Furthermore, the set of examples from which a verifier may choose is often infinite, whose elements may lead the synthesiser to search for less efficient programs.

The overall aim of this thesis is the development of new inductive synthesis theories and algorithms that (1) account for potentially incorrect descriptions and (2) intelligently select examples that are can direct the synthesis engine to efficient programs more quickly. For the former, the focus will be on the design of weakening and strengthening operators for repairing incorrect or partial descriptions in such a way that allows for new descriptions to be generated that (a) are semantically similar to the original ones, and (b) succeed in yielding a correct program. For the latter, new metrics will be defined to measure the goodness of an example with respect to the synthesis task.

The research underlying this thesis is aligned with EPSRC's software engineering research area.