Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Thursday, May 12, 2016 - 11:58:56 AM
Last modification on : Wednesday, November 3, 2021 - 8:09:34 AM
Long-term archiving on: : Wednesday, November 16, 2016 - 2:00:19 AM


Files produced by the author(s)


  • HAL Id : hal-01314876, version 1


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⟩



Record views


Files downloads