# SHF: Small: Optimizing runtime efficiency of symbolic execution for functional languages

> **NSF 01002526DB NSF RESEARCH & RELATED ACTIVIT** · SUNY at Binghamton (NY) · $321,874

## Abstract

As software enters more aspects of society, including financial institutions, medical devices, and autonomous vehicles, ensuring the absence of software bugs becomes increasingly important. Symbolic execution engines are tools that allow automatically finding bugs via mathematical reasoning. Unfortunately, symbolic execution of certain programs can be slow to the point where it is entirely ineffective. This project develops techniques to improve efficiency, thus allowing symbolic execution to be applied to a wider range of software. The project's novelties are in identifying problematic code patterns which slow down symbolic execution and developing new techniques which improve efficiency of symbolic execution of this code. The project's impacts are that symbolic execution will become applicable to a greater range of programs in domains where correctness is critical- such as finance and medicine- reducing the risk of costly software failures. In addition to developing the proposed techniques, the investigator plans to develop and teach a Software Verification & Formal Methods course, incorporating research developed under this grant into the course material where appropriate. Further, both graduate and undergraduate students will work on this project, introducing them to research and formal methods techniques. 

Symbolic execution engines work by treating some program inputs as symbolic variables and "running" the program with these unknown values. When the program branch

## Key facts

- **NSF award ID:** 2437952
- **Awardee organization:** SUNY at Binghamton (NY)
- **SAM.gov UEI:** NQMVAAQUFU53
- **PI:** William T Hallahan
- **Primary program:** 01002526DB NSF RESEARCH & RELATED ACTIVIT
- **All programs:** SMALL PROJECT, PROGRAMMING LANGUAGES
- **Estimated total:** $321,874
- **Funds obligated:** $321,874
- **Transaction type:** Standard Grant
- **Period:** 06/15/2025 → 05/31/2028

## Primary source

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

## Citation

> US National Science Foundation, Award 2437952, SHF: Small: Optimizing runtime efficiency of symbolic execution for functional languages. Retrieved via AI Analytics 2026-06-06 from https://api.ai-analytics.org/grant/nsf/2437952. Licensed CC0.

---

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