Specification and Proof of High-Level Functional Properties of Bit-Level ProgramsReport as inadecuate

Specification and Proof of High-Level Functional Properties of Bit-Level Programs - Download this document for free, or read online. Document in PDF available to download.

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

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.

Keywords : Deductive Verification Bit vector SMT solvers Functional specification

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

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


Related documents