TY - JOUR
AU - Appel, Andrew W.
AU - Bertot, Yves
PY - 2021/03/31
Y2 - 2021/04/16
TI - C floating-point proofs layered with VST and Flocq
JF - Journal of Formalized Reasoning
JA - JFR
VL - 13
IS - 1
SE -
DO - 10.6092/issn.1972-5787/11442
UR - https://jfr.unibo.it/article/view/11442
SP - 1-16
AB - <p>We demonstrate tools and methods for proofs about the correctness and numerical accuracy of C programs.<br /> The tools are <em>foundational,</em> in that they are connected to formal semantic specifications of the C operational semantics and of the IEEE 754 floating-point format. The tools are <em>modular</em>, in that the reasoning about C programming can be done quite separately from the reasoning about numerical correctness and numerical accuracy. The tools are <em>general</em>, in that they accommodate almost 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.</p>
ER -