Home |
Personal Info |
Papers |
Teaching |
Links |
Symbolic Path-Oriented Test Data Generation for Floating-Point Programs
Roberto Bagnara
BUGSENG and Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
Matthieu Carlier
INRIA Rennes Bretagne Atlantique
France
Roberta Gori
Dipartimento di Informatica
Università di Pisa
Corso Italia 40
I-56125 Pisa
Italy
Arnaud Gotlieb
Certus Software V&V Center
SIMULA Research Laboratory
P.O.Box 134, 1325 Lysaker
Norway
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 symbolic-execution test data generator tool.
Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, BibTeX entry.
[Page last updated on April 12, 2013, 18:30:32.]
bagnara@cs.unipr.it
Home | Personal | Papers | Teaching | Links