CAREER: Program Synthesis with Quantitative Guarantees

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

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.