CS2: Automatically Extracting High-Level Specifications from Large Scientific Codebases to Enhance Understandability and Correctness

Large scientific codebases cost millions of dollars to develop and support the work of countless computational scientists worldwide, so verifying their correctness is just as crucial as ensuring the proper functioning of expensive physical equipment in a "traditional" laboratory setting. However, unlike physical equipment, these codebases are built incrementally over decades, often by hundreds or thousands of different contributors, which creates ample opportunities for the unintentional introduction of bugs or security vulnerabilities. The goal of this project is to extract high-level specifications from large scientific codebases that concisely summarize their core functionality and enable automated correctness validation. The project's novelties are new techniques for performing such specification extraction in a scalable way by leveraging large language models (LLMs) in concert with more traditional formal methods. The project's impacts are: (1) improving confidence in and understandability of large scientific codebases; and (2) reducing reliance on current labor-intensive approaches like code reviews and unit testing. Concretely, this project introduces an extraction pipeline yielding specifications that are both succinct and executable. Succinctness not only increases understandability but also reduces the potential for elusive bugs lurking in low-level implementation details, whereas executability facilitates machine-checkable validation of correctness through provably sound and complete concolic property testing. Together, these features support the seamless porting or refactoring of the codebase without the risk of inadvertently introducing new errors. The pipeline relies on a flexible neuro-symbolic approach built around LLMs, with layers of guardrails to maintain correctness despite their propensity to hallucinate subtly incorrect answers. The end result is a human-in-the-loop process in which scientists and developers can work together with LLMs to iteratively refine the extracted specifications while avoiding most of the heavy lifting. 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. NSF Award ID: 2546694 | Program: 01002627DB NSF RESEARCH & RELATED ACTIVIT | Principal Investigator: Andrew Crotty | Institution: Northwestern University at Chicago, EVANSTON, IL | Award Amount: $200,000 View on NSF Award Search: https://www.nsf.gov/awardsearch/show-award/?AWD_ID=2546694 View on Research.gov: https://www.research.gov/awardapi-service/v1/awards/2546694.html