SHF: Foundations and Applications of Type-Based Under-Approximate Reasoning

Providing strong assurance arguments about program correctness has long been a critical issue in software development. This concern has become significantly more relevant given the growing popularity of AI-driven software generation tools whose code artifacts are rarely accompanied by the kinds of guarantees typically offered by modern testing or verification tools. To help overcome this challenge, this project proposes a principled integration of both over- and under-approximate reasoning methods, the former used to capture safety properties of a program that can be checked by verifiers, and the latter used to model reachability properties that guide testing and symbolic execution-based frameworks. The project's novelties center on new advances in type systems that enable a unified and compositional specification and validation framework to express and validate the claims made by these distinct approaches. The project's impacts are also multi-faceted, taking into consideration both theoretical as well as pragmatic aspects that build on these insights, with the goal of enabling significant improvements in software trustworthiness, automated reasoning, bug finding, and software maintainability. Central to the project's technical approach is the development of new foundations that provide a synergistic account of both safety (over-approximation) and reachability (under-approximation) in the presence of complex control- and data-flow (e.g., first-class functions), rich user-defined datatypes, concurrency, and state. These foundational advances inform the design, optimization, and implementation of tailored verification, synthesis, testing, and symbolic evaluation tools for realistic OCaml programs, a performant state-of-the-art industrial-strength programming language, which provides a feature-rich ecosystem well-suited to explore the project's core research aims. 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.