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

University Of Southern California, Los Angeles CA

Investigators

Abstract

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.