C floating-point proofs layered with VST and Flocq
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 t...
Main Authors: | , |
---|---|
Format: | Article |
Language: | English |
Published: |
University of Bologna
2021-03-01
|
Series: | Journal of Formalized Reasoning |
Online Access: | https://jfr.unibo.it/article/view/11442 |