Exploring the Boundaries of Solvable Program Synthesis

上下文和潜在影响程序合成描述了生成满足作为逻辑公式给出的规范的函数(即程序)的问题。简单地说明程序应该具有的属性(即程序应该做什么)，而不是自己对函数进行“编码”(即程序应该如何做)，这种能力有很多优点。其中一些是：正确性：显示程序正确性的通常方法需要编写程序，声明属性，最后显示所编写的程序遵守指定的属性。在程序综合中，首先说明所需的特性。在此之后，程序将自动构建。生成的程序通过构造是正确的(即遵守属性)，因此不需要任何进一步的步骤来证明正确性。独立性：经常需要编写重复的代码。由于操作系统或基础库的更改，可能会发生这种情况。然而，尽管所有这些更改可能需要更改程序，但它们不需要更改规范。因此，一个规范只需要声明一次，并且可以独立于底层系统重用。效率：制定程序应该做什么而不是如何做，通常需要相当少的时间。因此，使用程序综合可以显著加快开发过程。即使是这一有限的一组优势，也对软件开发和总体安全产生了重大影响。不幸的是，完全成熟的不受限制的程序合成在理论上是不可决定的，这在某种程度上并不令人惊讶。因此，大量的研究已经将程序综合问题限制在一个更简单且因此容易处理的问题上。其中一种方法被称为SyGuS(语法引导合成)。SyGuS规定了程序综合问题的一种格式，它由背景理论、通常以语法形式的句法约束和规范组成。背景理论为语法提供了语义，而规范则说明了要综合的函数的属性。由于上述原因，大多数研究都被放在可决定的背景理论中。尽管有这些限制，但在许多情况下，一般的SyGuS问题仍然无法确定，这使得合成工具在大多数情况下不完整或效率低下。然而，施加更多的句法限制使我们有可能在理论上可能和不可能之间行走。目的、目的和新奇在我们的研究中，我们试图继续对什么是可能的和不可能的进行理论研究。通过引入新的限制(在语法和语义中)并分析它们对SyGuS问题的易处理性的影响，我们希望更好地理解语法制导的合成及其限制。特别是，我们有以下目标：调查语法糖(例如ITE结构)对SyGuS问题可解性的影响。以LIA和LRA为背景理论对SyGuS进行更深入的分析。描述新的SyGuS问题类别，并结合从现有基准数据库中对问题进行分类来确定它们的易处理性。进一步，我们可以查看自动定理证明中已知的技术，如量词实例化，并研究它们在程序综合中的应用。此外，如果这些技术或限制中的一项被证明不仅易于处理而且还有用，我们还打算在最新的解决方案中加入解决这些SyGuS实例的过程。该项目属于EPSRC信息和通信技术(ICT)研究领域。我们计划与Sanjit Seshia合作。如果随后的结果具有实际应用价值，我们将尝试与Cesare Tinelli或Armando Solar-Lezama建立合作关系。

Context and Potential ImpactProgram 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 NoveltyIn 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.