| HAL-Inria | Publications, software ... of Inria's scientists |
Journal articles
C-language floating-point proofs layered with VST and Flocq
Abstract : We demonstrate tools and methods for proofs about the correctness and numerical accuracy of C programs. The tools are foundational, in that they are connected to formal semantic specifications of the C operational semantics and of the IEEE 754 floating-point format. Theools are modular, in that the reasoning about C programming can be done quite separately from the reasoning about numerical correctness and numerical accuracy. The tools are general, in that they accommodate amost the entire C language (with pointer data structures, function pointers, control flow, etc.) and applied mathematics (reasoned about in a general-purpose logic and proof assistant with substantial libraries for mathematical reasoning). We demonstrate on a simple Newton's-method square root function.
Keywords :
Floating point numbers
C programming language
https://hal.inria.fr/hal-03130704
Contributor : Yves Bertot <>
Submitted on : Monday, March 8, 2021 - 11:19:08 AM
Last modification on : Tuesday, March 9, 2021 - 3:27:23 AM
Contributor : Yves Bertot <>
Submitted on : Monday, March 8, 2021 - 11:19:08 AM
Last modification on : Tuesday, March 9, 2021 - 3:27:23 AM
File
paper_v2.pdf
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution 4.0 International License