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
Résumé : Dans un programme informatique, des fonctionalités de base sont parfois implémentées par des opérations bit-à-bit, par exemple à cause d'un besoin d'être proche de l'architecture matérielle sous-jacente, ou bien pour des questions d'efficacité, aussi bien en temps de calcul qu'en place mémoire. Si l'on cherche à spécifier formellement le comportement attendu d'un tel programme, il est souhaitable que la spécification se place à un niveau plus abstrait que celui des bits. Prouver formellement qu'un programme bas niveau est conforme à une spécification de plus haut niveau est un défi, à cause de l'écart important entre les niveaux d'abstraction en jeu. Notre approche pour résoudre ce défi consiste à concevoir une théorie formelle des vecteurs de bits, qui d'une part permet à un utilisateur d'écrire des spécifications proches d'un niveau de conception humain (ou bien disons, mathématique), et d'autre part peut se connecter aux procédures de décision et aux outils sachant traiter les vecteurs de bits, comme ceux qui sont développés dans le cadre SMT
Type de document :
Rapport
[Research Report] RR-8821, Inria Saclay. 2015, pp.52
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01238376
Contributeur : Claude Marché <>
Soumis le : vendredi 4 décembre 2015 - 17:19:53
Dernière modification le : vendredi 17 février 2017 - 16:10:35
Document(s) archivé(s) le : samedi 29 avril 2017 - 04:32:47

Fichier

RR-8821.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de
la notice

220

Téléchargements du document

184