Exploring the Boundaries of Solvable Program Synthesis

上下文和潜在影响程序综合描述了生成满足作为逻辑公式给出的规范的函数（即程序）的问题。简单地说明程序应该具有的属性（即程序应该做什么），而不是自己“编码”函数（即程序应该如何做某事）的能力有很多优点。其中一些是：正确性：显示程序正确性的通常途径需要编写程序，说明属性，最后显示所编写的程序符合指定的属性。在程序综合中，首先要说明所需的特性。然后，程序自动生成。这个结果程序在构造上是正确的（也就是说，遵守了属性），因此不需要任何进一步的步骤来证明正确性。独立性：经常会出现必须编写重复代码的情况。这可能是由于操作系统或底层库的更改而发生的。然而，虽然所有这些变化可能需要改变程序，但它们不需要改变规范。因此，一个规范只需要声明一次，并且可以独立于底层系统进行重用。效率：制定程序应该做什么而不是如何做，通常需要的时间要少得多。因此，使用程序合成可以大大加快开发过程，即使是这种有限的优势，也会对软件开发和安全产生重大影响。不幸的是，并不奇怪，完全成熟的无限制程序合成在理论上是不可判定的。因此，重要的研究已经进入限制程序综合问题，以一个更简单，因此易于处理的问题。其中一种方法被称为SyGuS（Syntax-guided Synthesis）。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.