CAREER: Underapproximate Refinement Types for Program Exploration and Understanding

Software development is rapidly changing, with developers increasingly delegating programming tasks to code generation tools powered by Large Language Models (LLMs). These systems often produce code that appears correct, but that actually contains subtle defects and inconsistencies with the developer’s intent, compromising the reliability and security of the generated program. As the role of software engineers moves away from writing code directly to inspecting generated programs, it is vital that they have trustworthy tools that help them rigorously examine and understand program behavior. Recent advances in formal methods have demonstrated that it is now possible to verify that complex real-world programs like compilers and operating systems behave exactly as intended. However, these tools are designed to confirm that a well-understood and correct program always does the right thing and are ill-suited to helping a developer explore and reason about a partially understood program that may contain flaws. The project’s novelties are the development of new, principled techniques for rigorously reasoning about the behaviors of potentially incorrect programs, and the creation of a trustworthy, general-purpose framework that helps developers effectively explore and understand such programs. The project’s impacts are increased trustworthiness and accountability in AI-assisted software development, supporting the responsible integration of AI code generation tools into larger software toolchains, and helping developers confidently deploy AI-generated software in safety- and security-critical domains. The major technical innovation of this work is a novel kind of type refinement that soundly captures the existence of certain paths that lead to errors, while soundly pruning those that are irrelevant to the property of interest. This type abstraction is capable of reasoning about the existence of “buggy” or undesirable executions and can soundly establish that a program is incorrect. The resulting reasoning framework leverages automated theorem provers to perform this analysis automatically and explores new modes of interacting with these solvers in the face of partial knowledge about a system. The educational goals of the project are to equip learners at all levels with principled reasoning techniques for understanding computer programs, emphasizing the foundations of automated and symbolic reasoning and their application to modern and AI-assisted software development. 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.