원문정보
초록
영어
We propose a local search based approach to generate automatically test cases for programs having floating point statements. The proposed approach, called MLFP (for Multi-precision arithmetic and Local search for Floating Point constraints), adopts a local search approach to solve constraints on floating point numbers. Compared to the classical integer domain, floating point numbers F have two particular properties: they have a huge cardinality (e.g., 252 numbers in the interval [0.5, 1.0] with the "double" format), huge values (e.g. 10300), and also tiny values (e.g. 10-300). This huge combinatorial nature of the search space motivates using a local search approach. In order to find test cases containing huge or tiny numbers, such as overflow or underflow exception errors, MLFP uses the multiple precision MPFR library. Our local search approach proceeds in two steps. The first step exploits a line search algorithm to converge quickly to an approximate solution on real numbers. The second step adopts a dedicated local search algorithm on floating point numbers in order to find an exact solution, by using specific neighborhood and evaluation functions. We have implemented the MLFP approach, and we have shown its usefulness on various non trivial programs having floating point statements.
목차
1. Introduction
2. Preliminaries
2.1. IEEE-754 Floating-Point Numbers Representation
2.2. Rounding Modes
2.3. Floating Point Exception Errors
2.4. Translating the Program Statements into a Constraint System
3. Test Case Generation as a Constraint Satisfaction Problem
3.1. The Final Constraint Satisfaction Problem
3.2. Illustration
4. MLFP Solving Approach
4.1. Approximate Solution by Line Search
4.2. A Dedicated Local Search Solving on Floating Point Numbers
5. Experiments
6. Conclusion
References