Abstract
We define several abstract semantics for the static analysis of finite precision computations, that bound not only the ranges of values taken by numerical variables of a program, but also the difference with the result of the same sequence of operations in an idealized real number semantics. These domains point out with more or less detail (control point, block, function for instance) sources of numerical errors in the program and the way they were propagated by further computations, thus allowing to evaluate not only the rounding error, but also sensitivity to inputs or parameters of the program. We describe two classes of abstractions, a non relational one based on intervals, and a weakly relational one based on parametrized zonotopic abstract domains called affine sets, especially well suited for sensitivity analysis and test generation. These abstract domains are implemented in the Fluctuat static analyzer, and we finally present some experiments.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Boldo, S., Filliâtre, J.-C.: Formal Verification of Floating-Point Programs. In: 18th IEEE International Symposium on Computer Arithmetic (June 2007)
Comba, J.L.D., Stolfi, J.: Affine arithmetic and its applications to computer graphics. In: SEBGRAPI 1993 (1993)
Conquet, E., Cousot, P., Cousot, R., Goubault, E., Ghorbal, K., Lesens, D., Putot, S., Turin, M.: Space software validation using abstract interpretation. In: Proceedings of DASIA (2009)
Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming, Dunod, Paris, France, pp. 106–130 (1976)
Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., Védrine, F.: Towards an industrial use of FLUCTUAT on safety-critical avionics software. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 53–69. Springer, Heidelberg (2009)
Zimmerman, P., et al.: The MPFR library, http://www.mpfr.org/
IEEE 754 Standard for Binary Floating-Point Arithmetic, revision (2008), http://ieeexplore.ieee.org/servlet/opac?punumber=4610933
Ghorbal, K., Goubault, E., Putot, S.: The zonotope abstract domain taylor1+. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 627–633. Springer, Heidelberg (2009)
Ghorbal, K., Goubault, E., Putot, S.: A logical product approach to zonotope intersection. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 212–226. Springer, Heidelberg (2010)
Goldberg, D.: What every computer scientist should know about floating-point arithmetic. ACM Comput. Surv. 23(1), 5–48 (1991)
Goubault, É.: Static analyses of the precision of floating-point operations. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 234–259. 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, É., Putot, S.: Weakly relational domains for the analysis of floating-point computations. Presented at NSAD (2005)
Goubault, É., Putot, S.: Static analysis of numerical algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 18–34. Springer, Heidelberg (2006)
Goubault, E., Putot, S.: Perturbed affine arithmetic for invariant computation in numerical program analysis. CoRR, abs/0807.2961 (2008)
Goubault, E., Putot, S.: A zonotopic framework for functional abstractions. CoRR, abs/0910.1763 (2009), http://arxiv.org/abs/0910.1763
Goubault, É., Putot, S., Baufreton, P., Gassino, J.: Static analysis of the accuracy in control systems: Principles and experiments. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 3–20. Springer, Heidelberg (2008)
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)
Meurant, G.: The Lanczos and Conjugate Gradient Algorithm; from theory to finite precision computation. SIAM, Philadelphia (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)
Miné, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348–363. Springer, Heidelberg (2005)
Monniaux, D.: The pitfalls of verifying floating-point computations. ACM Trans. Program. Lang. Syst. 30(3), 1–41 (2008)
Muller, J.-M.: Arithmétique des Ordinateurs. Masson (1989)
Muller, J.-M., Brisebarre, N., de Dinechin, F., Jeannerod, C.-P., Lefèvre, V., Melquiond, G., Revol, N., Stehlé, D., Torres, S.: Handbook of Floating-Point Arithmetic. Birkhäuser, Boston (2010)
APRON Project. Numerical abstract domain library (2007), http://apron.cri.ensmp.fr
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)
Skeel, R.: Roundoff error and the patriot missile. SIAM News (1992)
Sterbenz, P.H.: Floating point computation. Prentice-Hall, Englewood Cliffs (1974)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goubault, E., Putot, S. (2011). Static Analysis of Finite Precision Computations. In: Jhala, R., Schmidt, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2011. Lecture Notes in Computer Science, vol 6538. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-18275-4_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-18275-4_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-18274-7
Online ISBN: 978-3-642-18275-4
eBook Packages: Computer ScienceComputer Science (R0)