Name
Abstract | ||
|---|---|---|
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.
|
Year | DOI | Venue |
|---|---|---|
2016 | 10.1145/2854065.2854066 | CPP 2016: Certified Proofs and Programs
St. Petersburg
FL
USA
January, 2016 |
Keywords | Field | DocType |
Formal Verification, Coq, Floating-point Computations, C | Expression (mathematics),Floating point,Computer science,Round-off error,Algorithm,Theoretical computer science,Formal specification,Rounding,Square root,IEEE floating point,Formal verification | Conference |
ISBN | Citations | PageRank |
978-1-4503-4127-1 | 4 | 0.39 |
References | Authors | |
18 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tahina Ramananandro | 1 | 78 | 7.64 |
| Paul Mountcastle | 2 | 4 | 0.39 |
| Benoît Meister | 3 | 138 | 12.84 |
| Richard Lethin | 4 | 118 | 17.17 |