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

Clément Fumex 1, 2 Claire Dross 3 Jens Gerlach 4 Claude Marché 2, 1
1 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. 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.
Type de document :
Communication dans un congrès
NASA Formal methods, Jun 2016, Minneapolis, United States. Springer, 2016, NASA Formal methods
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01314876
Contributeur : Claude Marché <>
Soumis le : jeudi 12 mai 2016 - 11:58:56
Dernière modification le : vendredi 17 février 2017 - 16:10:44
Document(s) archivé(s) le : mercredi 16 novembre 2016 - 02:00:19

Fichier

article-final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. Springer, 2016, NASA Formal methods. 〈hal-01314876〉

Partager

Métriques

Consultations de
la notice

219

Téléchargements du document

161