EAGER: Duality-Based Algorithm Synthesis

设计一种算法来执行期望的功能或实现期望的目标，目前需要问题领域的专业知识。因此，尽管人们可以使用强大的计算平台，但大多数非专业人士仅限于通过预编程的应用程序使用这些平台。通过使计算机能够将问题的高级说明转换为可计算的过程，自动程序合成改变了这种现状。除了使技术为更多人所接受的好处之外，程序合成还有望减少错误，提高软件的性能。程序综合是指发现满足用户指定要求的程序的问题。一般来说，这是一个很难解决的问题。然而，如果可能程序的空间是有限的，那么迭代地搜索可能程序的空间以寻找在所有输入上都能正确工作的某个程序就变得可行了。在这种普遍存在的公式中量词的交替使得综合计算变得困难，并且阻碍了可扩展性。该项目通过开发和利用编程中的对偶概念，极大地提高了程序综合的效率。计算和证明之间的对偶性承诺在理解程序分析和综合方面发挥基础作用。它不仅包含了几个众所周知的概念，如类型、抽象和抽象解释，而且还超越了这些概念，提供了一种将证明附加到程序中的通用方法。对偶性允许通过一个相对更易于处理的存在约束来近似所有存在的合成约束。该项目开发了基于二元性的综合方法。该项目还通过免费分发工具和包括研究生实习在内的学术访问计划，为教育、研究和技术向工业转移做出贡献。

The task of designing an algorithm that performs a desired function, or achieves a desired goal, currently requires expertise in the problem domain. Consequently, although people have access to powerful computing platforms, most non-experts are limited to using these platforms through pre-programmed apps. Automated program synthesis changes this current state of affairs by enabling computers to convert high-level specification of the problem to a computable procedure. Apart from the benefit of making technology accessible to more people, program synthesis has the promise of reducing errors, and improving performance, of software. Program synthesis refers to the problem of discovering a program that meets the requirements specified by a user. It is a hard problem to solve in general. However, if the space of possible programs is restricted, then it becomes feasible to iteratively search the space of possible programs for some program that works correctly on all inputs. The quantifier alternation in this exists-forall formulation makes synthesis computationally difficult and hinders scalability. This project drastically improves efficiency of program synthesis by developing and exploiting a notion of duality in programming. Duality between computing and proving promises to play a foundational role in understanding program analysis and synthesis. It not only encompasses several well-known concepts, such as types, abstractions, and abstract interpretation, but also goes beyond them to provide a general methodology for attaching a proof with a program. Duality enables approximating the exists-forall synthesis constraint by a relatively more tractable exists-constraint. This project develops the duality-based synthesis approach. This project also makes contributions to education, research, and technology transfer to industry through freely distributed tools and academic visitor programs that include internships for graduate students.