CAREER: The Next 700 Solver-Aided Languages

职业：未来 700 种求解器辅助语言

• 批准号: 1651225
• 负责人: Emina Torlak
• 金额: $ 49.86万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-02-01 至 2022-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1651225&HistoricalAwards=false
• 关键词: CAREER; Next; 700; Solver; Aided

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.

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

项目成果

Synthesizing interpretable strategies for solving puzzle games

综合解决益智游戏的可解释策略

• DOI: 10.1145/3102071.3102084
• 发表时间: 2017
• 期刊: Proceedings of the International Conference on the Foundations of Digital Games - FDG '17
• 作者: Butler, Eric;Torlak, Emina;Popović, Zoran
• 通讯作者: Popović, Zoran

Refinement Types for Ruby

Ruby 的细化类型

• 发表时间: 2018
• 期刊: and Abstract Interpretation - VMCAI'18
• 作者: Kazerounian, Milod;Vazou, Niki;Bourgerie, Austin;Foster, Jeff;Torlak, Emina
• 通讯作者: Torlak, Emina

A Framework for Computer-Aided Design of Educational Domain Models

• DOI: 10.1007/978-3-319-73721-8_7
• 发表时间: 2018-01
• 作者: Eric Butler;Emina Torlak;Zoran Popovic

Symbolic types for lenient symbolic execution

用于宽松符号执行的符号类型

• DOI: 10.1145/3158128
• 发表时间: 2017
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Chang, Stephen;Knauth, Alex;Torlak, Emina
• 通讯作者: Torlak, Emina

Finding Code That Explodes under Symbolic Evaluation

• DOI: 10.1145/3276519
• 发表时间: 2018-11-01
• 期刊: PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL
• 影响因子: 1.8
• 作者: Bornholt, James;Torlak, Emina
• 通讯作者: Torlak, Emina