CAREER: Program Synthesis with Quantitative Guarantees

职业：具有定量保证的程序合成

基本信息

批准号：
1750965
负责人：
Loris DAntoni
金额：
$ 50万
依托单位：
University of Wisconsin-Madison
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
2018
资助国家：
美国
起止时间：
2018-09-01 至 2024-08-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1750965&HistoricalAwards=false
关键词：
CAREER Program Synthesis Quantitative Guarantees

项目摘要

Software has been changing our lives for many decades, but despite the advances in programming language design, how we write programs has not changed much: programmers keep repeating similar mistakes, writing similar programs, and fixing similar bugs. Program synthesis, the art of automatically generating programs that meet user intents, promises to increase the productivity of programmers and end-users of computing devices by automating tedious, error-prone, and time-consuming tasks. Despite the practical successes of program synthesis, we still do not have systematic frameworks to synthesize programs that are good according to certain metrics-e.g., produce programs of a reasonable size or with good running time-and to understand when synthesis can result in such good programs. This project investigates the problem of performing program synthesis in the presence of quantitative objectives while providing quantitative guarantees on the results and on the performance of the synthesis algorithms. This project investigates new formal methods such as weighted grammars and weighted logics, to specify quantitative objectives on the syntax, semantics, and probabilistic outcomes of the synthesized programs, as well as new synthesis algorithms for solving problems expressible in such formalisms. The proposed work will lead to more predictable, accurate, and robust synthesis algorithms, which will be integrated widely used synthesis applications such as tools for personalized education, network synthesis, programming by examples, and automated program repair. The investigator will organize a series of lectures about the impact of program synthesis on the labor force and will lead several diversity and outreach efforts to undergraduates, women, under-represented minorities, and non-traditional students.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

几十年来，软件一直在改变我们的生活，但尽管编程语言设计取得了进步，但我们编写程序的方式并没有太大改变：程序员不断重复类似的错误，编写类似的程序，修复类似的错误。程序合成是自动生成满足用户意图的程序的艺术，它有望通过自动化繁琐、容易出错且耗时的任务来提高程序员和计算设备最终用户的生产力。尽管程序综合在实践中取得了成功，但我们仍然没有系统的框架来综合根据某些指标（例如，生成合理大小或具有良好运行时间的程序）良好的程序，并了解综合何时可以产生如此好的结果程序。该项目研究了在存在定量目标的情况下执行程序综合的问题，同时为结果和综合算法的性能提供定量保证。该项目研究新的形式方法，例如加权语法和加权逻辑，以指定合成程序的语法、语义和概率结果的定量目标，以及用于解决以此类形式主义表达的问题的新合成算法。拟议的工作将带来更可预测、更准确和更稳健的综合算法，这些算法将集成广泛使用的综合应用程序，例如个性化教育工具、网络综合、示例编程和自动程序修复。调查员将组织一系列关于项目综合对劳动力影响的讲座，并将领导针对本科生、女性、代表性不足的少数族裔和非传统学生的多项多元化和外展工作。该奖项反映了 NSF 的法定使命，并已通过使用基金会的智力优点和更广泛的影响审查标准进行评估，被认为值得支持。