Software — free catalog

PRECiSA with Instrumented Code Generation

A NASA software catalog entry available for reuse or request.

Find it in the NASA software catalog Open project or source

About this technology

Overview

PRECiSA (Program Round-off Certifier via Static Analysis) is a fully automatic static analyzer for floating-point valued functions. It computes an over-approximation of the round-off error of a given floating-point expression, along with a formal certificate that ensures the correctness of the estimated error.