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

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

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.