Symbolic execution of floating-point computations

Bernard Botella 1 Arnaud Gotlieb 2 Claude Michel 3
2 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Symbolic execution is a classical program testing technique which evaluates a selected control flow path with symbolic input data. A constraint solver can be used to enforce the satisfiability of the extracted path conditions as well as to derive test data. Whenever path conditions contain floating-point computations, a common strategy consists of using a constraint solver over the rationals or the reals. Unfortunately, even in a fully IEEE-754 compliant environment, this leads not only to approximations but also can compromise correctness: a path can be labelled as infeasible although there exists floating-point input data that satisfy it. In this paper, we address the peculiarities of the symbolic execution of program with floating-point numbers. Issues in the symbolic execution of this kind of programs are carefully examined and a constraint solver is described that supports constraints over floating-point numbers. Preliminary experimental results demonstrate the value of our approach.
Type de document :
Article dans une revue
Software Testing Verification and Reliability, John Wiley & Sons, Ltd, 2006, 16 (2), pp.97-121. 〈10.1002/stvr.333〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00540299
Contributeur : Arnaud Gotlieb <>
Soumis le : mercredi 1 décembre 2010 - 10:01:43
Dernière modification le : vendredi 13 janvier 2017 - 14:18:21
Document(s) archivé(s) le : mercredi 2 mars 2011 - 02:30:34

Fichiers

stvr.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Bernard Botella, Arnaud Gotlieb, Claude Michel. Symbolic execution of floating-point computations. Software Testing Verification and Reliability, John Wiley & Sons, Ltd, 2006, 16 (2), pp.97-121. 〈10.1002/stvr.333〉. 〈inria-00540299〉

Partager

Métriques

Consultations de
la notice

349

Téléchargements du document

284