Skip to main content

C floating-point proofs layered with VST and Flocq

Author(s): Appel, Andrew W; Bertot, Yves

To refer to this page use:
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.
Publication Date: 2020
Citation: Appel, Andrew W., Yves Bertot. "C floating-point proofs layered with VST and Flocq." Journal of Formalized Reasoning 13, no. 1 (2020): pp. 1-16. doi:10.6092/issn.1972-5787/11442
EISSN: 1972-5787
Pages: 1 - 16
Type of Material: Journal Article
Journal/Proceeding Title: Journal of Formalized Reasoning
Version: Final published version. Article is made available in OAR by the publisher's permission or policy.

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.