Abstract
We present a new numerical abstract domain for static analysis of the errors introduced by the approximation by floating-point arithmetic of real numbers computation, by abstract interpretation [3]. This work extends a former domain [4,8], with an implicitly relational domain for the approximation of the floating-point values of variables, based on affine arithmetic [2]. It allows us to analyze non trivial numerical computations, that no other abstract domain we know of can analyze with such precise results, such as linear recursive filters of different orders, Newton methods for solving non-linear equations, polynomial iterations, conjugate gradient algorithms.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Blanchet, B., Cousot, P.R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI 2003 (2003)
Stolfi, J., de Figueiredo, L.H.: An introduction to affine arithmetic. TEMA Tend. Mat. Apl. Comput. 4(3), 297–312 (2003)
Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Symbolic Computation 2(4), 511–547 (1992)
Goubault, É.: Static analyses of the precision of floating-point operations. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, p. 234. Springer, Heidelberg (2001)
Goubault, É., Martel, M., Putot, S.: Asserting the precision of floating-point computations: A simple abstract interpreter. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 209–212. Springer, Heidelberg (2002)
Goubault, E., Martel, M., Putot, S.: Some future challenges in the validation of control systems. In: European Symposium on Real-Time Systems ERTS 2006 (2006)
Sankaranarayanan, S., Colón, M.A., Sipma, H.B., Manna, Z.: Efficient strongly relational polyhedral analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 111–125. Springer, Heidelberg (2005)
Martel, M.: Propagation of roundoff errors in finite precision computations: A semantics approach. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 194–208. Springer, Heidelberg (2002)
Miné, A.: The octagon abstract domain. Journal of Higher-Order and Symbolic Computation (to appear, 2006)
Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004)
MPFR library Documentation and downloadable library at: http://www.mpfr.org
Putot, S., Goubault, É., Martel, M.: Static analysis-based validation of floating-point computations. In: Alt, R., Frommer, A., Kearfott, R.B., Luther, W. (eds.) Dagstuhl Seminar 2003. LNCS, vol. 2991, pp. 306–313. Springer, Heidelberg (2004)
Putot, S., Goubault, E.: Weakly relational domains for floating-point computation analysis. In: Proceedings of NSAD 2005 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goubault, E., Putot, S. (2006). Static Analysis of Numerical Algorithms. In: Yi, K. (eds) Static Analysis. SAS 2006. Lecture Notes in Computer Science, vol 4134. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11823230_3
Download citation
DOI: https://doi.org/10.1007/11823230_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37756-6
Online ISBN: 978-3-540-37758-0
eBook Packages: Computer ScienceComputer Science (R0)