Abstract
We present lightweight and generic symbolic methods to improve the precision of numerical static analyses based on Abstract Interpretation. The main idea is to simplify numerical expressions before they are fed to abstract transfer functions. An important novelty is that these simplifications are performed on-the-fly, using information gathered dynamically by the analyzer.
A first method, called “linearization,” allows abstracting arbitrary expressions into affine forms with interval coefficients while simplifying them. A second method, called “symbolic constant propagation,” enhances the simplification feature of the linearization by propagating assigned expressions in a symbolic way. Combined together, these methods increase the relationality level of numerical abstract domains and make them more robust against program transformations. We show how they can be integrated within the classical interval, octagon and polyhedron domains. These methods have been incorporated within the Astrée static analyzer that checks for the absence of run-time errors in embedded critical avionics software. We present an experimental proof of their usefulness.
This work was partially supported by the Astrée RNTL project and the APRON project from the ACI “Sécurité & Informatique.”
This is a preview of subscription content, log in via an institution to check access.
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
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: ACM PLDI 2003, vol. 548030, pp. 196–207. ACM Press, New York (2003)
Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Pottosin, I.V., Bjorner, D., Broy, M. (eds.) FMP&TA 1993. LNCS, vol. 735, pp. 128–114. Springer, Heidelberg (1993)
Clarisó, R., Cortadella, J.: The octahedron abstract domain. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 312–327. Springer, Heidelberg (2004)
Colby, C.: Semantics-Based Program Analysis via Symbolic Composition of Transfer Relations. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA (1996)
Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: ISOP 1976, Dunod, Paris, France, pp. 106–130 (1976)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM POPL 1977, pp. 238–252. ACM Press, New York (1977)
Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. Journal of Logic Programming 13(2–3), 103–179 (1992)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: ACM POPL 1978, pp. 84–97. ACM Press, New York (1978)
Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004)
Granger, P.: Improving the results of static analyses programs by local decreasing iteration. In: Shyamasundar, R.K. (ed.) FSTTCS 1992. LNCS, vol. 652, pp. 68–79. Springer, Heidelberg (1992)
Kildall, G.: A unified approach to global program optimization. In: ACM POPL 1973, pp. 194–206. ACM Press, New York (1973)
Miné, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001, pp. 310–319. IEEE CS Press, Los Alamitos (2001)
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.: Weakly Relational Numerical Abstract Domains. PhD thesis, École Polytechnique, Palaiseau, France (december 2004)
Simon, A., King, A., Howe, J.: Two variables per linear inequality as an abstract domain. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 71–89. Springer, Heidelberg (2003)
Vinícius, M., Andrade, A., Comba, J.L.D., Stolfi, J.: Affine arithmetic. In: INTERVAL 1994 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miné, A. (2005). Symbolic Methods to Enhance the Precision of Numerical Abstract Domains. In: Emerson, E.A., Namjoshi, K.S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2006. Lecture Notes in Computer Science, vol 3855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11609773_23
Download citation
DOI: https://doi.org/10.1007/11609773_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31139-3
Online ISBN: 978-3-540-31622-0
eBook Packages: Computer ScienceComputer Science (R0)