Symbolic methods to enhance the precision of numerical abstract domains. (English) Zbl 1176.68050
Emerson, E. Allen (ed.) et al., Verification, model checking, and abstract interpretation. 7th international conference, VMCAI 2006, Charleston, SC, USA, January 8–10, 2006. Proceedings. Berlin: Springer (ISBN 3-540-31139-4/pbk). Lecture Notes in Computer Science 3855, 348-363 (2006).
Summary: 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.
For the entire collection see [Zbl 1097.68002].
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.
For the entire collection see [Zbl 1097.68002].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68W30 | Symbolic computation and algebraic computation |
