C floating-point proofs layered with VST and Flocq

Authors

  • Andrew W. Appel Princeton University
  • Yves Bertot INRIA Sophia-Antipolis

DOI:

https://doi.org/10.6092/issn.1972-5787/11442

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. 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.

Downloads

Published

2020-12-21 — Updated on 2021-03-31

Versions

How to Cite

Appel, A. W., & Bertot, Y. (2021). C floating-point proofs layered with VST and Flocq. Journal of Formalized Reasoning, 13(1), 1-16. https://doi.org/10.6092/issn.1972-5787/11442 (Original work published December 21, 2020)

Issue

Section

Articles