CAREER: Foundations of Statistical Program Reasoning

University Of Southern California, Los Angeles CA

Investigators

Abstract

This award is funded in whole or in part under the American Rescue Plan Act of 2021 (Public Law 117-2). Program analysis and verification systems are both challenging to design and expensive to operate, with a reputation for poor scalability, false warnings, and missed bugs. In addition, these program-reasoning tools interoperate poorly with the continuous and iterative nature of modern software engineering processes, and only have rudimentary ways of interacting with human engineers. The project develops techniques to extend the underlying deductive basis of these analyses---commonly expressed using declarative formalisms such as constrained Horn clauses (CHCs) or Datalog---with probabilistic modes of reasoning. These probabilistic models provide a mechanism to prioritize warnings, incorporate feedback from developers, and combine knowledge from multiple analysis tools. As such, the project's main impact is to significantly improve the accuracy and usability of program analysis technology. The project develops algorithms to automatically learn probabilistic models from analysis of implementations, and determine their accuracy using open-source code corpora such as GitHub and databases such as Common Vulnerabilities and Exposures (CVE). Next, it develops ranking techniques to optimize effective accuracy, time needed to discover bugs, and other programmer-specified relevance criteria. The project introduces new interfaces for users to interact with program analysis algorithms, indicate preferences, and provide feedback on ground truth. For the analysis user, the project builds new bug-finding tools that provide useful, actionable insight into their programs. For analysis designers, the project offers new ways to apply statistical techniques in program verification, and new opportunities to produce accurate and scalable program analysis systems. 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.