×

Relational abstract domain of weighted hexagons. (English) Zbl 1342.68082

Miné, Antoine (ed.) et al., Proceedings of the 2nd international workshop on numerical and symbolic abstract domains: NSAD 2010, Perpignan, France, September 13, 2010. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 267, No. 1, 59-72 (2010).
Summary: We propose a new numerical abstract domain for static analysis by abstract interpretation, the domain of weighted hexagons. It is capable of expressing interval constraints and relational invariants of the form \(x \leq a \cdot y\), where \(x\) and \(y\) are variables and \(a\) denotes a non-negative constant. This kind of domain is useful in analysis of safety for array accesses when multiplication is used (e.g., in guarding formulæ or in access expressions). We provide all standard abstract domain operations, including widening operator, as well as a graph-based algorithm for checking satisfiability and computing normal form for elements of the domain. All described operations are performed in \(O(n^{3})\) time. Expressiveness of this domain lies between the pentagons by Logozzo and Fähndrich and the two variables per inequality by Simon, King and Howe.
For the entire collection see [Zbl 1284.68022].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

ASTREE
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Balasundaram, V.; Kennedy, K., A technique for summarizing data access and its use in parallelism enhancing transformations, SIGPLAN Not., 24, 41-53 (1989)
[2] Blanchet, B., P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux and X. Rival, A static analyzer for large safety-critical software, in: PLDI’03 (2003), pp. 196-207.; Blanchet, B., P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux and X. Rival, A static analyzer for large safety-critical software, in: PLDI’03 (2003), pp. 196-207. · Zbl 1026.68514
[3] Bourdoncle, F., Abstract debugging of higher-order imperative languages, in: PLDI’93 (1993), pp. 46-55.; Bourdoncle, F., Abstract debugging of higher-order imperative languages, in: PLDI’93 (1993), pp. 46-55.
[4] Cormen, T. H.; Leiserson, C. E.; Rivest, R. L., Introduction to Algorithms (1990), MIT Press · Zbl 1158.68538
[5] Cousot, P., Design of syntactic program transformations by abstract interpretation of semantic transformations, in: Proceedings of the 17th International Conference on Logic Programming (2001), pp. 4-5.; Cousot, P., Design of syntactic program transformations by abstract interpretation of semantic transformations, in: Proceedings of the 17th International Conference on Logic Programming (2001), pp. 4-5. · Zbl 1053.68561
[6] Cousot, P. and R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: POPL’77 (1977), pp. 238-252.; Cousot, P. and R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: POPL’77 (1977), pp. 238-252.
[7] Cousot, P. and R. Cousot, Static determination of dynamic properties of recursive procedures, in: E. Neuhold, editor, IFIP Conf. on Formal Description of Programming Concepts, St-Andrews, N.B., CA (1977), pp. 237-277.; Cousot, P. and R. Cousot, Static determination of dynamic properties of recursive procedures, in: E. Neuhold, editor, IFIP Conf. on Formal Description of Programming Concepts, St-Andrews, N.B., CA (1977), pp. 237-277. · Zbl 0393.68080
[8] Cousot, P. and R. Cousot, Systematic design of program analysis frameworks, in: POPL’79 (1979), pp. 269-282.; Cousot, P. and R. Cousot, Systematic design of program analysis frameworks, in: POPL’79 (1979), pp. 269-282. · Zbl 1323.68356
[9] Cousot, P.; Cousot, R., Abstract interpretation and application to logic programs, J. Log. Program., 13, 103-179 (1992) · Zbl 0776.68024
[10] Cousot, P. and N. Halbwachs, Automatic discovery of linear restraints among variables of a program, in: POPL’78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages (1978), pp. 84-96.; Cousot, P. and N. Halbwachs, Automatic discovery of linear restraints among variables of a program, in: POPL’78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages (1978), pp. 84-96.
[11] Logozzo, F. and M. Fähndrich, Pentagons: a weakly relational abstract domain for the efficient validation of array accesses, in: SAC’08 (2008), pp. 184-188.; Logozzo, F. and M. Fähndrich, Pentagons: a weakly relational abstract domain for the efficient validation of array accesses, in: SAC’08 (2008), pp. 184-188.
[12] Miné, A., The octagon abstract domain, Higher Order Symbolic Computation, 19, 31-100 (2006) · Zbl 1105.68069
[13] Simon, A., A. King and J. M. Howe, Two variables per linear inequality as an abstract domain, in: LOPSTR’02: Proceedings of the 12th international conference on Logic based program synthesis and transformation (2003), pp. 71-89.; Simon, A., A. King and J. M. Howe, Two variables per linear inequality as an abstract domain, in: LOPSTR’02: Proceedings of the 12th international conference on Logic based program synthesis and transformation (2003), pp. 71-89. · Zbl 1278.68072
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.