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

Publication TypeConference Paper
Year of Publication2013
AuthorsBagnara R, Carlier M, Gori R, Gotlieb A
Conference NameProceedings of the 6th IEEE International Conference on Software Testing, Verification and Validation
PublisherIEEE Press
Conference LocationLuxembourg City, Luxembourg
ISBN Number978-0-7695-4968-2/13
Keywordsfloating-point, IEEE 754, testing, verification

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 symbolic-execution test data generator tool.

File attachments: 
We are a passionate team of experts. Do not hesitate to let us have your feedback:
You may be surprised to discover just how much your suggestions matter to us.