@article{Appel_Bertot_2020, title={C floating-point proofs layered with VST and Flocq}, volume={13}, url={https://jfr.unibo.it/article/view/11442}, DOI={10.6092/issn.1972-5787/11442}, abstractNote={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. 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 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.}, number={1}, journal={Journal of Formalized Reasoning}, author={Appel, Andrew W. and Bertot, Yves}, year={2020}, month={Jan.}, pages={1–16} }