TY - JOUR
T1 - C-language oating-point proofs layered with VST and Flocq
AU - Appel, Andrew W.
AU - Bertot, Yves
N1 - Funding Information:
We thank Michael Soegtrop for assistance in configuring CompCert, Flocq, and VST. We thank Laurence Rideau and Guillaume Melquiond for their help in navigating the Flocq library. This research was supported in part by National Science Foundation grant CCF-1521602.
Funding Information:
We thank Michael Soegtrop for assistance in configuring CompCert, Flocq, and VST. We thank Laurence Rideau and Guillaume Melquiond for their help in navigatingthe Flocq library. This research was supported in part by National Science Foundation grant CCF-1521602
Publisher Copyright:
© 2020. All rights reserved.
PY - 2020
Y1 - 2020
N2 - 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 specciations of the C operational semantics and of the IEEE 754 oating-point format. The tools 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 almost the entire C language (with pointer data structures, function pointers, control ow, 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.
AB - 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 specciations of the C operational semantics and of the IEEE 754 oating-point format. The tools 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 almost the entire C language (with pointer data structures, function pointers, control ow, 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.
UR - http://www.scopus.com/inward/record.url?scp=85101357325&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85101357325&partnerID=8YFLogxK
M3 - Article
AN - SCOPUS:85101357325
SN - 1972-5787
VL - 13
SP - 1
EP - 16
JO - Journal of Formalized Reasoning
JF - Journal of Formalized Reasoning
IS - 1
ER -