Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-00807884
Contributor : Arnaud Gotlieb <>
Submitted on : Thursday, April 4, 2013 - 3:11:23 PM
Last modification on : Tuesday, June 15, 2021 - 4:26:36 PM
Long-term archiving on: : Friday, July 5, 2013 - 4:18:26 AM

File

ICST2013_Symbolic_Path-Oriente...
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-00807884⟩

Share

Metrics

Record views

905

Files downloads

463