# CAREER: Underapproximate Refinement Types for Program Exploration and Understanding

> **NSF 01002627DB NSF RESEARCH & RELATED ACTIVIT** · Purdue University (IN) · $673,078

## Abstract

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

## Key facts

- **NSF award ID:** 2542188
- **Awardee organization:** Purdue University (IN)
- **SAM.gov UEI:** YRXVL4JYCEF5
- **PI:** Benjamin J Delaware
- **Primary program:** 01002627DB NSF RESEARCH & RELATED ACTIVIT
- **All programs:** Artificial Intelligence (AI), CAREER-Faculty Erly Career Dev, PROGRAMMING LANGUAGES
- **Estimated total:** $673,078
- **Funds obligated:** $391,123
- **Transaction type:** Continuing Grant
- **Period:** 09/01/2026 → 08/31/2031

## Primary source

NSF Award Search: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2542188

## Citation

> US National Science Foundation, Award 2542188, CAREER: Underapproximate Refinement Types for Program Exploration and Understanding. Retrieved via AI Analytics 2026-07-19 from https://api.ai-analytics.org/grant/nsf/2542188. Licensed CC0.

---

*[NSF Awards dataset](/datasets/nsf-awards) · CC0 1.0*