CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016

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.

Mon 18 Jan

10:30 - 12:00: CPP - Session 2: Verifying Imperative Programs at Room St Petersburg II
CPP-2016-main145310940000010:30 - 11:00
CPP-2016-main145311120000011:00 - 11:30
CPP-2016-main145311300000011:30 - 12:00
Peter LammichTechnische Universität München