Symbolic Path-Oriented Test Data Generation for Floating-Point Programs

Abstract : Verifying critical numerical software involves the generation of test data for floating-point intensive programs. As the symbolic execution of floating-point computations presents significant difficulties, existing approaches usually resort to random or search-based test data generation. However, without symbolic reasoning, it is almost impossible to generate test inputs that execute many paths with floating-point computations. Moreover, constraint solvers over the reals or the rationals do not handle the rounding errors. In this paper, we present a new version of FPSE, a symbolic evaluator for C program paths, that specifically addresses this problem. The tool solves path conditions containing floating-point computations by using correct and precise projection functions. This version of the tool exploits an essential filtering property based on the representation of floating-point numbers that makes it suitable to generate path-oriented test inputs for complex paths characterized by floating-point intensive computations. The paper reviews the key implementation choices in FPSE and the labeling search heuristics we selected to maximize the benefits of enhanced filtering. Our experimental results show that FPSE can generate correct test inputs for selected paths containing several hundreds of iterations and thousands of executable floating-point statements on a standard machine: this is currently outside the scope of any other symbolicexecution test data generator tool.
Type de document :
Communication dans un congrès
Proc. of the 6th IEEE Int. Conf. on Software Testing, Verification and Validation (ICST'13), Mar 2013, Luxembourg, Luxembourg. 2013
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00807884
Contributeur : Arnaud Gotlieb <>
Soumis le : jeudi 4 avril 2013 - 15:11:23
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : vendredi 5 juillet 2013 - 04:18:26

Fichier

ICST2013_Symbolic_Path-Oriente...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00807884, version 1

Citation

Roberto Bagnara, Matthieu Carlier, Roberta Gori, Arnaud Gotlieb. Symbolic Path-Oriented Test Data Generation for Floating-Point Programs. Proc. of the 6th IEEE Int. Conf. on Software Testing, Verification and Validation (ICST'13), Mar 2013, Luxembourg, Luxembourg. 2013. 〈hal-00807884〉

Partager

Métriques

Consultations de la notice

721

Téléchargements de fichiers

235