Specification and Proof of High-Level Functional Properties of Bit-Level Programs

Abstract : In a computer program, basic functionalities may be implemented using bit-wise operations. To formally specify the expected behavior of such a low-level program, it is desirable that the specification should be at a more abstract level. Formally proving that low-level code conforms to a higher-level specification is challenging, because of the gap between the different levels of abstraction. We address this challenge by designing a rich formal theory of fixed-sized bit vectors , which on the one hand allows a user to write abstract specifications close to the human—or mathematical—level of thinking, while on the other hand permits a close connection to decision procedures and tools for bit vectors, as they exist in the context of the Satisfiability Modulo Theory framework. This approach is implemented in the Why3 environment for deductive program verification, and also in its front-end environment SPARK for the development of safety-critical Ada programs. We report on several case studies used to validate our approach.
Document type :
Conference papers
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01314876
Contributor : Claude Marché <>
Submitted on : Thursday, May 12, 2016 - 11:58:56 AM
Last modification on : Monday, October 7, 2019 - 5:18:01 PM
Long-term archiving on : Wednesday, November 16, 2016 - 2:00:19 AM

File

article-final.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01314876, version 1

Citation

Clément Fumex, Claire Dross, Jens Gerlach, Claude Marché. Specification and Proof of High-Level Functional Properties of Bit-Level Programs. NASA Formal methods, Jun 2016, Minneapolis, United States. ⟨hal-01314876⟩

Share

Metrics

Record views

433

Files downloads

1371