# Collaborative Research: CS2: A Comprehensive Pipeline for Formal Verification of Floating-Point Errors and Compilation for Scientific Computing

> **NSF 01002526DB NSF RESEARCH & RELATED ACTIVIT** · Regents of the University of Michigan - Ann Arbor (MI) · $750,000

## Abstract

Scientific computing (SC) involves using advanced computing capabilities to understand and solve complex physical problems. With the increasing complexity of physical models and a rise in demand for high-performance computing (HPC) resources, errors can occur at all levels of abstraction in the computing process, significantly impacting the process of computer driven-scientific discovery and decision-making. Thus, correctness in scientific computing remains a formidable challenge. Prior works have attempted to verify a numerical program end-to-end but fall short in terms of scalability in the proof process, and target an idealized implementation of a numerical program. This project addresses this gap by developing a scalable verification framework, which directly targets application SC libraries written in Low Level Virtual Machine (LLVM)-compatible programming languages, like C/C++, Fortran and Julia, instead of an idealized implementation. The project's novelties are mechanized functional models for SC algorithms, accuracy and stability proofs of critical numerical algorithms in reduced- and mixed-precision floating-point (FP) formats, and the development of evidence and assurance cases for guaranteed correctness of future ports to new accelerated hardware. The project's impacts are an increased productivity of model developers, by providing a framework for root cause analysis of numerical bugs, and strong assurance cases for highly performant SC applications. 

This pr

## Key facts

- **NSF award ID:** 2446214
- **Awardee organization:** Regents of the University of Michigan - Ann Arbor (MI)
- **SAM.gov UEI:** GNJ7BBP73WE9
- **PI:** Jean-Baptiste Jeannin
- **Primary program:** 01002526DB NSF RESEARCH & RELATED ACTIVIT
- **All programs:** —
- **Estimated total:** $750,000
- **Funds obligated:** $750,000
- **Transaction type:** Standard Grant
- **Period:** 06/15/2025 → 05/31/2029

## Primary source

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

## Citation

> US National Science Foundation, Award 2446214, Collaborative Research: CS2: A Comprehensive Pipeline for Formal Verification of Floating-Point Errors and Compilation for Scientific Computing. Retrieved via AI Analytics 2026-06-08 from https://api.ai-analytics.org/grant/nsf/2446214. Licensed CC0.

---

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