Specification and Proof of High-Level Functional Properties of Bit-Level Programs - Archive ouverte HAL Access content directly
Conference Papers Year : 2016

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

(1, 2) , (3) , (4) , (2, 1)
1
2
3
4

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.
Fichier principal
Vignette du fichier
article-final.pdf (156.95 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01314876 , version 1 (12-05-2016)

Identifiers

  • HAL Id : hal-01314876 , version 1

Cite

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⟩
306 View
1139 Download

Share

Gmail Facebook Twitter LinkedIn More