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 |