Finding Round-Off Error Using Symbolic Execution

  • Anh-Hoang Truong
  • Huy-Vu Tran
  • Bao-Ngoc Nguyen
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 244)


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.


Arithmetic Operation Execution Path Path Condition Symbolic Execution Symbolic Expression 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Goldberg, D.: What Every Computer Scientist Should Know About Floating-Point Arithmetic. ACM Computing Surveys, 5–48 (1991)Google Scholar
  2. 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. 3.
    Higham, N.J.: Accuracy and Stability of Numerical Algorithms. SIAM: Society for Industrial and Applied Mathematics (2002)Google Scholar
  4. 4.
    King, J.C., Watson, J.: Symbolic Execution and Program Testing. Communications of the ACM, 385–394 (1976)Google Scholar
  5. 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. 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. 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. 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. 9.
    Smith, J.B.: Practical OCaml (Practical). Apress, Berkely (2006)Google Scholar
  10. 10.
    Stallings, W.: Computer Organization and Architecture. Macmillan Publishing Company (2000)Google Scholar
  11. 11.
    Stolfi, J., de Figueiredo, L.H.: An introduction to affine arithmetic. In: Tendencias em Matematica Aplicada e Computacional (2005)Google Scholar
  12. 12.
    Wolfram, S.: Mathematica: A System for Doing Mathematics by Computer. Addison-Wesley (1991)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Anh-Hoang Truong
    • 1
  • Huy-Vu Tran
    • 1
  • Bao-Ngoc Nguyen
    • 1
  1. 1.VNU University of Engineering and TechnologyHanoiVietnam

Personalised recommendations