CAREER: The Next 700 Solver-Aided Languages

软件是现代基础设施的重要组成部分，编程是许多领域知识工作的重要组成部分，从物理学到生物学再到社会科学。然而，将算法和想法转化为代码并不是一件容易的事，错误可能会付出代价。脚本中的错误可能使科学结果无效，文件系统中的错误可能导致灾难性的数据丢失。该项目通过一种新颖的编程方法使系统程序员和科学家更容易编程，该方法使用求解器辅助工具自动化特定领域语言（DSL）进行程序验证和合成。知识的优点是推进知识的编程支持特定领域的验证和合成，在共同设计的语言和工具，并在应用求解器辅助编程到新的领域。该项目的更广泛的意义和重要性是将求解器辅助编程的范围扩大了几个数量级，并扩展到数千名程序员，促进具有社会，教育和工业影响的新应用。该项目的关键思想是使验证和综合工具，这通常是由计算机科学博士手工制作的，像DSL一样简单，由广泛的程序员开发。PI先前在求解器辅助语言方面的工作已经证明了这是可能的，使从专业开发人员到高中生的各种程序员能够快速构建各种领域的综合和验证工具，从放射治疗软件到低功耗计算再到K-12教育。由此产生的工具是基于可满足性模理论（SMT）解决方案的简化，因此，依赖于（1）从根本上难以处理的技术，（2）需要多年的经验和培训才能有效使用。因此，本提案的目标是解决求解器辅助编程的核心挑战：使非专家能够诊断和优化求解器辅助工具的性能。为了实现这一目标，该项目开发了以下自动化技术：（1）符号分析，以提供有关求解器辅助堆栈中可扩展性瓶颈原因的诊断信息;（2）符号优化，以通过代码重构，（Meta）草图挖掘和求解引擎的组合来缓解已识别的可扩展性瓶颈;以及（3）作为评估符号剖析和优化的新挑战问题的应用，以及作为吸引从计算机架构师到教育专家的不同用户群体的演示。

Software is a critical part of modern infrastructure, and programming is an essential part of knowledge work in many fields, from physics to biology to social science. Yet translating algorithms and ideas into code is no easy task, and mistakes can be costly. A bug in a script can invalidate scientific results, and a bug in a file system can cause catastrophic loss of data. This project makes programming easier for systems programmers and scientists alike, through a novel approach to programming that automates domain-specific languages (DSLs) with solver-aided tools for program verification and synthesis. The intellectual merits are to advance knowledge in programming support for domain-specific verification and synthesis, in co-design of languages and tools, and in applying solver-aided programming to new domains. The project's broader significance and importance are to extend the reach of solver-aided programming by orders of magnitude and to thousands of programmers, facilitating new applications with societal, educational, and industrial impact.The project's key idea is to make verification and synthesis tools, which are usually hand-crafted by computer science PhDs, as simple to build as DSLs, which are developed by a broad spectrum of programmers. The PI's prior work on solver-aided languages has demonstrated that this is possible, enabling a wide range of programmers, from professional developers to high-school students, to rapidly construct synthesis and verification tools for a variety of domains, from radiation therapy software to low-power computing to K-12 education. The resulting tools are based on reduction to Satisfiability Modulo Theories (SMT) solving, and as such, rely on technology that is (1) fundamentally intractable and (2) requires years of experience and training to use effectively. The goal of this proposal is thus to address the central challenge of solver-aided programming: enabling non-experts to diagnose and optimize the performance of solver-aided tools. To achieve this goal, the project develops automatic techniques for (1) symbolic profiling to provide diagnostic information about the causes of scalability bottlenecks across the solver-aided stack; (2) symbolic optimization to mitigate the identified scalability bottlenecks via code refactoring, (meta)sketch mining, and combination of solving engines; and (3) applications to serve as new challenge problems for evaluating symbolic profiling and optimization, and as demos for attracting a diverse population of users, from computer architects to education experts.