A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
Tahina Ramananandro, Paul Mountcastle, Benoît Meister and Richard Lethin (Reservoir Labs Inc.)
- Final version (at ACM Digital Library)
- Paper preprint
- Conference slides
- Coq libraries: VCFloat, verified SAR backprojection
Please note that the C implementation of SAR backprojection certified in this publicly available version of Verified SAR-BP is only based on sin, cos and sqrt all assumed to be correctly rounded in double-precision floating-point numbers, and does not use any of the patent-pending and/or otherwise patent-protected approximations of square root, norm and sine described in Sections 5.1 and 5.3 of the abovementioned CPP 2016 paper. Please contact me (removing NOS and PAM) to access the latter proof on these patent-protected technologies.
We provide concrete evidence that floating-point computations in C programs can be verified in a homogeneous verification setting based on Coq only, by evaluating the practicality of the combination of the formal semantics of CompCert Clight and the Flocq formal specification of IEEE 754 floating-point arithmetic for the verification of properties of floating-point computations in C programs. To this end, we develop a framework to automatically compute real-number expressions of C floating-point computations with rounding error terms along with their correctness proofs. We apply our framework to the complete analysis of an energy-efficient C implementation of a radar image processing algorithm, for which we provide a certified bound on the total noise introduced by floating-point rounding errors and energy-efficient approximations of square root and sine.