High-Level Functional Properties of Bit-Level Programs: Formal Specifications and Automated Proofs

Claire Dross 1 Clément Fumex 2, 3 Jens Gerlach 4 Claude Marché 2, 3
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : In a computer program, basic functionalities may be implemented using bit-wise operations. This can be motivated by the need to be close to the underlying architecture, or the need of efficiency, both in term of time and memory space. If one wants 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 a low-level code conforms to a higher-level specification is challenging, because of the gap between the different levels of abstraction. Our approach to address this challenge is to design 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 experimentally.
Document type :
Reports
Liste complète des métadonnées

Cited literature [33 references]  Display  Hide  Download

https://hal.inria.fr/hal-01238376
Contributor : Claude Marché <>
Submitted on : Friday, December 4, 2015 - 5:19:53 PM
Last modification on : Thursday, April 5, 2018 - 12:30:22 PM
Document(s) archivé(s) le : Saturday, April 29, 2017 - 4:32:47 AM

File

RR-8821.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01238376, version 1

Citation

Claire Dross, Clément Fumex, Jens Gerlach, Claude Marché. High-Level Functional Properties of Bit-Level Programs: Formal Specifications and Automated Proofs. [Research Report] RR-8821, Inria Saclay. 2015, pp.52. ⟨hal-01238376⟩

Share

Metrics

Record views

333

Files downloads

298