Finding Round-Off Error Using Symbolic Execution
Overflow and round-off error has been a research problem for decades. With the explosion of mobile and embedded devices, many software programs written for personal computer are now ported to run on embedded systems. The porting often requires changing floating-point numbers and operations to fixed-point ones and here round-off error between the two versions of the program occurs. We propose a novel approach that uses symbolic computation to produce a precise representation of the round-off error for a program. Then we can use solvers to find a global optimum of the round-off error symbolic expression as well as to generate test data that cause the worst round-off error. We implemented a tool based on the idea and our experimental results are better than recent related work.
KeywordsArithmetic Operation Execution Path Path Condition Symbolic Execution Symbolic Expression
Unable to display preview. Download preview PDF.
- 1.Goldberg, D.: What Every Computer Scientist Should Know About Floating-Point Arithmetic. ACM Computing Surveys, 5–48 (1991)Google Scholar
- 2.Goldsztejn, A., Daney, D., Rueher, M., Taillibert, P.: Modal intervals revisited: a mean-value extension to generalized intervals. In: Proc. of the 1st International Workshop on Quantification in Constraint Programming (2005)Google Scholar
- 3.Higham, N.J.: Accuracy and Stability of Numerical Algorithms. SIAM: Society for Industrial and Applied Mathematics (2002)Google Scholar
- 4.King, J.C., Watson, J.: Symbolic Execution and Program Testing. Communications of the ACM, 385–394 (1976)Google Scholar
- 5.Martel, M.: Semantics of roundoff error propagation in finite precision calculations. In: Higher-Order and Symbolic Computation, pp. 7–30 (2006)Google Scholar
- 6.Ngoc, D.T.B., Ogawa, M.: Overflow and Roundoff Error Analysis via Model Checking. In: Conference on Software Engineering and Formal Methods, pp. 105–114 (2009)Google Scholar
- 7.Ngoc, D.T.B., Ogawa, M.: Combining Testing and Static Analysis to Overflow and Roundoff Error Detection. In: JAIST Research Reports, pp. 105–114 (2010)Google Scholar
- 8.Pham, T.-H., Truong, A.-H., Chin, W.-N., Aoshima, T.: Test Case Generation for Adequacy of Floating-point to Fixed-point Conversion. In: Proceedings of the 3rd International Workshop on Harnessing Theories for Tool Support in Software (TTSS). ENTCS, vol. 266, pp. 49–61 (2010)Google Scholar
- 9.Smith, J.B.: Practical OCaml (Practical). Apress, Berkely (2006)Google Scholar
- 10.Stallings, W.: Computer Organization and Architecture. Macmillan Publishing Company (2000)Google Scholar
- 11.Stolfi, J., de Figueiredo, L.H.: An introduction to affine arithmetic. In: Tendencias em Matematica Aplicada e Computacional (2005)Google Scholar
- 12.Wolfram, S.: Mathematica: A System for Doing Mathematics by Computer. Addison-Wesley (1991)Google Scholar