Skip to Main content Skip to Navigation
Journal articles

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
3 Laboratoire d'Informatique, Signaux, et Systèmes de Sophia-Antipolis (I3S) / Equipe CEP
Laboratoire I3S - MDSC - Modèles Discrets pour les Systèmes Complexes
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.
Document type :
Journal articles
Complete list of metadata

Cited literature [37 references]  Display  Hide  Download
Contributor : Arnaud Gotlieb Connect in order to contact the contributor
Submitted on : Wednesday, December 1, 2010 - 10:01:43 AM
Last modification on : Wednesday, June 30, 2021 - 9:58:04 AM
Long-term archiving on: : Wednesday, March 2, 2011 - 2:30:34 AM


Files produced by the author(s)



Bernard Botella, Arnaud Gotlieb, Claude Michel. Symbolic execution of floating-point computations. Journal of : Software Testing, Verification and Reliability, Wiley, 2006, 16 (2), pp.97-121. ⟨10.1002/stvr.333⟩. ⟨inria-00540299⟩



Record views


Files downloads