Name
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\u0027s-method square root function. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.6092/issn.1972-5787/11442 | Journal of Formalized Reasoning |
DocType | Volume | Issue |
Journal | 13 | 1 |
ISSN | Citations | PageRank |
1972-5787 | 0 | 0.34 |
References | Authors | |
0 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andrew W. Appel | 1 | 2599 | 292.71 |
| Yves Bertot | 2 | 442 | 40.82 |