项目来源

美国国家科学基金(NSF)

项目主持人

Loris D'Antoni

项目受资助机构

UNIVERSITY OF CALIFORNIA SAN DIEGO

项目编号

2506134

财政年度

2025,2022

立项时间

未公开

研究期限

未知 / 未知

项目级别

国家级

受资助金额

1619494.00美元

学科

未公开

学科代码

未公开

基金类别

Standard Grant

关键词

Software&Hardware Foundation ; MEDIUM PROJECT ; Formal Methods and Verification

参与者

Thomas Reps

参与机构

UNIVERSITY OF CALIFORNIA,SAN DIEGO

项目标书摘要：The field of program synthesis aims to create tools that can automatically create a program from a specification of desired behavior.Synthesis holds the promise of easing the burden on programmers(e.g.,by finding solutions to tricky special cases automatically),and allowing non-programmers to create programs merely by indicating the outcome that they want the program to produce.Unfortunately,current synthesis tools do not scale up to large-scale programming problems,a situation that threatens to doom this promising technology to being a niche field.This project's novelties are ways to exploit compositionality in program synthesis in a way that allows one to create bigger programs out of smaller ones.The project builds on a recent framework called SemGuS(Semantics-Guided Synthesis),which offers a foothold on the expressibility and scalability problems of program synthesis.In principle,the framework can support the synthesis of software in layers,where implementation choices in one layer are hidden from other layers(and thus consistent with modular software design with information hiding).The goal of the project is to capitalize on the opportunity that SemGuS offers for extending synthesis to much larger systems than was possible heretofore.The work will lead to more scalable and general synthesis algorithms,with potential benefits to synthesis applications that are already in widespread use.Further development of the SemGuS framework has the potential to make synthesis more usable and programmable,and thereby allow users to carry out synthesis tasks without prior knowledge of existing synthesis tools.Most importantly,compositional synthesis will allow synthesis to scale to larger applications with more practical relevance.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.

人员信息

Loris DAntoni(Principal Investigator)：ldantoni@ucsd.edu；

机构信息

【University of California-San Diego(Performance Institution)】StreetAddress：9500 GILMAN DR,LA JOLLA,California,United States/ZipCode：920930021；【UNIVERSITY OF CALIFORNIA,SAN DIEGO】StreetAddress：9500 GILMAN DR,LA JOLLA,California,United States/PhoneNumber：8585344896/ZipCode：920930021；

项目主管部门

Directorate for Computer and Information Science and Engineering(CSE)-Division of Computing and Communication Foundations(CCF)

项目官员

Anindya Banerjee(Email：abanerje@nsf.gov；Phone：7032927885)