https://jfr.unibo.it/ <strong>Journal of Formalized Reasoning (JFR) – ISSN 1972-5787</strong> encourages submission of papers describing significant, automated or semi-automated formalization efforts in any area, including classical mathematics, constructive mathematics, formal algorithms, and program verification. The emphasis of the journal is on proof techniques and methodologies and their impact on the formalization process. In particular, the journal provides a forum for comparing alternative approaches, enhancing reusability of solutions and offering a clear view of the current state of the field. en-US <p>Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.</p><div><a href="http://creativecommons.org/licenses/by/3.0/" rel="license"><img src="https://i.creativecommons.org/l/by/3.0/88x31.png" alt="Creative Commons License" /></a></div><p>This journal is licensed under a <a href="http://creativecommons.org/licenses/by/3.0/" rel="license">Creative Commons Attribution 3.0 Unported License</a> (<a href="http://creativecommons.org/licenses/by/3.0/legalcode">full legal code</a>). <br />See also our <a href="/about/editorialPolicies#openAccessPolicy">Open Access policy</a></p> sacerdot@cs.unibo.it (Prof. Claudio Sacerdoti Coen) ojs@unibo.it (OJS Support) Mon, 21 Dec 2020 18:32:51 +0100 OJS 3.2.1.4 http://blogs.law.harvard.edu/tech/rss 60 https://jfr.unibo.it/article/view/12643 Andrew W. Appel, Yves Bertot Copyright (c) 2020 Andrew W. Appel, Yves Bertot http://creativecommons.org/licenses/by/3.0 https://jfr.unibo.it/article/view/12643 Wed, 31 Mar 2021 00:00:00 +0200 https://jfr.unibo.it/article/view/11442 <p>We demonstrate tools and methods for proofs about the correctness and numerical accuracy of C programs.<br /> The tools are <em>foundational,</em> 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 <em>modular</em>, in that the reasoning about C programming can be done quite separately from the reasoning about numerical correctness and numerical accuracy. The tools are <em>general</em>, 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.</p> Andrew W. Appel, Yves Bertot Copyright (c) 2020 Andrew W. Appel, Yves Bertot http://creativecommons.org/licenses/by/3.0 https://jfr.unibo.it/article/view/11442 Wed, 31 Mar 2021 00:00:00 +0200