C-language oating-point proofs layered with VST and Flocq

Andrew W. Appel, Yves Bertot

Research output: Contribution to journalArticlepeer-review

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

Original languageEnglish (US)
Pages (from-to)1-16
Number of pages16
JournalJournal of Formalized Reasoning
Volume13
Issue number1
StatePublished - 2020

All Science Journal Classification (ASJC) codes

  • Computer Science (miscellaneous)
  • Mathematics(all)

Fingerprint

Dive into the research topics of 'C-language oating-point proofs layered with VST and Flocq'. Together they form a unique fingerprint.

Cite this