Formal Methods Seminar
Title: PRECiSA: A Static Analysis Tool for Floating-Point Programs
Speaker: Laura Titolo, Staff Scientist, NIA
Date: Friday, November 2, 2018
Time: 10:30am
Location: B1230, R264A
Abstract: Floating-point numbers are the most common finite representation of real numbers in computer programs and they offer a good trade-off between efficiency and precision. However, in safety-critical systems, round-off errors due to floating-point operations may be unacceptably large and have catastrophic consequences. In this talk, we present PRECiSA: a static analysis tool that is able to compute verified round-off error bounds for floating-point programs. The tool is based on a denotational semantics that computes a symbolic estimation of the floating-point round-off error along with a proof certificate that ensures its correctness and can be automatically discharged in the PVS theorem prover. This symbolic estimation can be evaluated on concrete inputs using rigorous enclosure methods to produce formally verified numerical error bounds. Abstract interpretation techniques are used in PRECiSA to mitigate the state explosion and to ensure the convergence of recursive functions.