权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

CRII: SHF: RUI: Exploring Human-in-the-loop Program Synthesis Through Live Coding

CRII：SHF：RUI：通过实时编码探索人机循环程序合成

基本信息

批准号：
2105208
负责人：
Mark Santolucito
金额：
$ 17.33万
依托单位：
Barnard College
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2021
资助国家：
美国
起止时间：
2021-05-01 至 2025-04-30
项目状态：
未结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2105208&HistoricalAwards=false
关键词：
CRII SHF RUI Exploring Human

项目摘要

Program synthesis is a formal technique that promises to decrease software development costs, decrease the risk of software bugs, and make programming skills more accessible to a broader audience. Yet for all the development of theory and techniques in this area, the adoption of program synthesis by users has been limited. A key hurdle in expanding the impact of synthesis is that fully automated software synthesis does not match the iterative software design process that is used in practice. The majority of existing techniques strive to be fully automated, acting as black-boxes for users: the user provides a specification and the tool returns complete program code. The investigators propose to overcome this hurdle through human-in-the-loop synthesis which allows a user to incrementally refine specifications and code through interaction with the synthesis engine. This project focuses on developing techniques and theories that increase the adoption of program synthesis in real-world systems. They use a performative practice from the computer-music community, called Live Coding, in which users write code that generates music (or other media) in real-time. This project formalizes human-in-the-loop Program Synthesis and its intersection with Live Coding, and develops new human-in-the-loop program-synthesis techniques. The investigators explore the use of these techniques in Live Coding and other settings. This project will also provide the opportunity for female undergraduates to participate in computer-science research - many for the first time.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.

程序合成是一种形式化的技术，它有望降低软件开发成本，降低软件错误的风险，并使编程技能更容易为更广泛的受众所接受。然而，在这一领域的理论和技术的所有发展，程序合成的用户采用一直是有限的。扩展综合影响的一个关键障碍是，全自动软件综合与实际使用的迭代软件设计过程不匹配。大多数现有的技术都致力于完全自动化，对用户来说就像黑盒一样：用户提供规范，工具返回完整的程序代码。研究人员建议通过人在回路合成来克服这一障碍，该合成允许用户通过与合成引擎的交互来逐步完善规范和代码。这个项目的重点是开发技术和理论，增加在现实世界的系统中采用程序合成。他们使用计算机音乐社区的表演实践，称为Live Coding，用户编写代码实时生成音乐（或其他媒体）。该项目形式化了人在回路程序合成及其与Live Coding的交叉，并开发了新的人在回路程序合成技术。研究人员探索这些技术在Live Coding和其他环境中的使用。该项目还将为女大学生提供参与计算机科学研究的机会--其中许多是第一次。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

期刊论文数量（6）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Towards the Usability of Reactive Synthesis: Building Blocks of Temporal Logic

迈向反应综合的可用性：时态逻辑的构建块

DOI：
发表时间：
2023
期刊：
Plateau Workshop.
影响因子：
0
作者：
Rothkopf, Raven;Cui, Angel Leyi;Zeng, Hannah Tongxin;Sinha, Arya;Santolucito. Mark
通讯作者：
Santolucito. Mark

Can reactive synthesis and syntax-guided synthesis be friends?

反应式合成和语法引导合成可以成为朋友吗？

DOI：
10.1145/3519939.3523429
发表时间：
2022
期刊：
PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
影响因子：
0
作者：
Choi, Wonhyuk;Finkbeiner, Bernd;Piskac, Ruzica;Santolucito, Mark
通讯作者：
Santolucito, Mark

Program Synthesis for Musicians: A Usability Testbed for Temporal Logic Specifications

音乐家的程序综合：时间逻辑规范的可用性测试台