Collaborative Research: SHF: Medium: Synthesis of Logic Programs for Democratizing Program Analysis

合作研究：SHF：媒介：民主化程序分析的逻辑程序综合

• 批准号: 2107261
• 负责人: Mukund Raghothaman
• 金额: $ 48万
• 依托单位: University of Southern California
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-05-01 至 2025-04-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2107261&HistoricalAwards=false
• 关键词: Collaborative; Research; SHF; Medium; Synthesis

Despite massive advances in program-analysis techniques, the diversity of situations in which software development occurs -- including programming environments and application domains -- has created a large community of programmers who are under-served by existing analysis, verification, and bug-finding tools. The investigators are leveraging advances in relational program representations and declarative query-synthesis methods to develop novel interactive systems by which software developers can identify bugs and security vulnerabilities in code. The main impact of this research will be to increase the accessibility of program analysis technology to the working programmer.The proposed system is exposing a rich example-based interface, and is driven by a range of synthesis techniques involving constraint solvers, provenance trackers, and co-occurrence relationships among the entities of the program. The project is developing example-guided synthesis algorithms, exploring approaches to synthesize recursive programs, and devising component-based frameworks by which to assemble complex program analyzers from libraries of simple constituent analyses. Furthermore, the investigators are developing methods to automatically extract the necessary relational data from compiler infrastructure such as LLVM, and to connect their algorithms to widely supported programming environment interfaces such as the Language Server Protocol (LSP), thus maximizing the utility of the proposed research to a broad range of software developers. The project is mentoring and training undergraduate and doctoral students, including female and under-represented minorities. Finally, the research and pedagogical artifacts developed in the project are being disseminated to software developers and researchers through workshops, tutorials, and courses.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.

尽管程序分析技术取得了巨大的进步，但软件开发所处的各种情况（包括编程环境和应用程序领域）已经创造了一个庞大的程序员社区，他们无法得到现有分析、验证和缺陷查找工具的服务。 研究人员正在利用关系程序表示和声明式查询合成方法的进步来开发新的交互式系统，软件开发人员可以通过该系统识别代码中的错误和安全漏洞。 这项研究的主要影响将是增加程序分析技术的可访问性的工作programmer.The建议的系统是暴露一个丰富的基于实例的接口，并由一系列的综合技术，包括约束求解器，出处跟踪器，和程序的实体之间的共现关系。 该项目正在开发示例引导的合成算法，探索合成递归程序的方法，并设计基于组件的框架，通过该框架从简单成分分析库中组装复杂的程序分析器。 此外，研究人员正在开发从编译器基础设施（如LLVM）中自动提取必要的关系数据的方法，并将其算法连接到广泛支持的编程环境接口（如语言服务器协议（LSP）），从而最大限度地提高所提出的研究对广泛软件开发人员的效用。 该项目正在指导和培训本科生和博士生，包括女性和代表人数不足的少数群体。最后，在项目中开发的研究和教学工件正在通过研讨会，教程和课程传播给软件开发人员和研究人员。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Example-guided synthesis of relational queries

• DOI: 10.1145/3453483.3454098
• 发表时间: 2021-06
• 期刊: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
• 作者: Aalok Thakkar;Aaditya Naik;Nathaniel Sands;R. Alur;M. Naik;Mukund Raghothaman

Sporq: An Interactive Environment for Exploring Code using Query-by-Example

• DOI: 10.1145/3472749.3474737
• 发表时间: 2021-10
• 期刊: The 34th Annual ACM Symposium on User Interface Software and Technology
• 作者: Aaditya Naik;Jonathan Mendelson;Nathaniel Sands;Yuepeng Wang;M. Naik;Aalok Thakkar;Nathaniel Sands;Mukund Raghothaman;Mukund Ragothaman