A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
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 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
10:30 - 12:00
|Higher-order Representation Predicates in Separation Logic|
|A Unified Coq Framework for Verifying C Programs with Floating-Point Computations|
|Refinement Based Verification of Imperative Data Structures|
Peter Lammich Technische Universität München