en fr High-Level Functional Properties of Bit-Level Programs: Formal Specifications and Automated Proofs Propriétés fonctionnelles de haut-niveau pour des programmes opérant au niveau des bits: spécifications formelles et preReport as inadecuate




en fr High-Level Functional Properties of Bit-Level Programs: Formal Specifications and Automated Proofs Propriétés fonctionnelles de haut-niveau pour des programmes opérant au niveau des bits: spécifications formelles et pre - Download this document for free, or read online. Document in PDF available to download.

1 AdaCore SAS - AdaCore SAS 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 3 LRI - Laboratoire de Recherche en Informatique 4 Fraunhofer FOKUS

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.

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 entemps de calcul qu-en place mémoire. Si l-on cherche à spécifierformellement le comportement attendu d-un tel programme, il estsouhaitable que la spécification se place à un niveau plus abstraitque celui des bits. Prouver formellement qu-un programme bas niveauest 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éorieformelle des vecteurs de bits, qui d-une part permet à un utilisateurd-écrire des spécifications proches d-un niveau de conception humainou bien disons, mathématique, et d-autre part peut se connecter auxprocédures de décision et aux outils sachant traiter les vecteurs de bits,comme ceux qui sont développés dans le cadre SMT

en fr

Keywords : Formal specification deductive verification formal proof fixed-size bit-vectors

Mots-clés : Spécification formelle preuve de programmes vecteurs de bits





Author: Claire Dross - Clément Fumex - Jens Gerlach - Claude Marché -

Source: https://hal.archives-ouvertes.fr/



DOWNLOAD PDF




Related documents