CAREER: Program Synthesis with 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.