×

Widening and narrowing operators for abstract interpretation. (English) Zbl 1218.68100

Summary: Abstract interpretation, one of the most applied techniques for semantics based static analysis of software, is based on two main key-concepts: the correspondence between concrete and abstract semantics through Galois connections/insertions, and the feasibility of a fixed point computation of the abstract semantics, through the fast convergence of widening operators. The latter point is crucial to ensure the scalability of the analysis to large software systems. The aim of this paper is to set the ground for a systematic design of widening and narrowing operators, by comparing the different definitions introduced in the literature and by discussing how to tune them in case of domain abstraction and domains’ combination through cartesian and reduced products.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing

Software:

cc(FD)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bagnara, R.; Hill, P. M.; Ricci, E.; Zaffanella, E., Precise widening operators for convex polyhedra, Science of Computer Programming, 58, 1-2, 28-56 (2005) · Zbl 1088.68173
[2] Bagnara, R.; Hill, P. M.; Zaffanella, E., Widening operators for powerset domains, Software Tools for Technology Transfer, 8, 4/5, 449-466 (2006)
[3] Bagnara, R.; Hill, P. M.; Mazzi, E.; Zaffanella, E., Widening operators for weakly-relational numeric abstractions, (Static analysis: proceedings of the 12th international symposium. Lecture notes in computer science, vol. 3672 (2005), Springer-Verlag), 3-18 · Zbl 1141.68445
[4] Birkhoff, G., Lattice theory (1973), American Mathematical Society Colloquium Publications: American Mathematical Society Colloquium Publications Rhode Island · Zbl 0126.03801
[5] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, et al. A static analyzer for large safety-critical software. In: PLDI ’03: Proceedings of the ACM SIGPLAN 2003 conference on Programm, k MING language design and implementation, 2003. p. 196-207.; Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, et al. A static analyzer for large safety-critical software. In: PLDI ’03: Proceedings of the ACM SIGPLAN 2003 conference on Programm, k MING language design and implementation, 2003. p. 196-207. · Zbl 1026.68514
[6] Choi T-H, Lee O, Kim H, Doh K-G. A practical string analyzer by the widening approach. In: APLAS, 2006. p. 374-88.; Choi T-H, Lee O, Kim H, Doh K-G. A practical string analyzer by the widening approach. In: APLAS, 2006. p. 374-88. · Zbl 1168.68359
[7] Cortesi, A., Widening operators for abstract interpretation, (SEFM ’08: proceedings of the 2008 sixth IEEE international conference on software engineering and formal methods (2008), IEEE Computer Society: IEEE Computer Society Los Alamitos, CA, USA), 31-40
[8] Cortesi, A.; Le Charlier, B.; Van Hentenryck, P., Combinations of abstract domains for logic programming: open product and generic pattern construction, Science of Computer Programming, 38, 1-3, 27-71 (2000) · Zbl 0957.68023
[9] Cortesi, A.; Filé, G.; Ranzato, F.; Giacobazzi, R.; Palamidessi, C., Complementation in abstract interpretation, ACM Transactions on Programming Languages and Systems, 19, 1, 7-47 (1997)
[10] Cortesi, A.; Filé, G.; Winsborough, W., The quotient of an abstract interpretation, Theoretical Computer Science, 202, 1-2, 163-192 (1998) · Zbl 0902.68030
[11] Cousot, P., Proving the absence of run-time errors in safety-critical avionics code, (Kirsch, C.; Wilhelm, R., Proceedings of the seventh ACM & IEEE international conference on embedded software, embedded systems (EMSOFT 2007) (2007), ACM Press: ACM Press Salzburg, Austria), 7-9
[12] Cousot P, Cousot R. Static determination of dynamic properties of programs. In: Proceedings of the second international symposium on programming, Dunod, Paris, France, 1976. p. 106-30.; Cousot P, Cousot R. Static determination of dynamic properties of programs. In: Proceedings of the second international symposium on programming, Dunod, Paris, France, 1976. p. 106-30. · Zbl 0393.68080
[13] Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, (Conference record of the sixth annual ACM SIGPLAN-SIGACT symposium on principles of programming languages (1979), ACM Press: ACM Press San Antonio, Texas, New York, NY), 269-282 · Zbl 0788.68094
[14] Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, (Sixth ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL ’79) (1979), ACM Press), 269-282 · Zbl 0788.68094
[15] Cousot, P.; Cousot, R., Abstract interpretation frameworks, Journal of Logic and Computation, 2, 4, 511-547 (1992) · Zbl 0783.68073
[16] Cousot, P.; Cousot, R., Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, (Proceedings of the international workshop on programming language implementation and logic programming. Lecture notes in computer science, vol. 631 (1992), Springer-Verlag), 269-295
[17] Cousot, P.; Halbwachs, N., Automatic discovery of linear restraints among variables of a program, (Fifth ACM SIGPLAN-SIGACT symposium on principles of programming languages (1978), ACM Press), 84-97
[18] Davey, B. A.; Priestley, H. A., Introduction to lattices and order (1990), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0701.06001
[19] D’Silva V. Widening for automata. PhD thesis, Institut fur Informatik, Universitaat Zurich; 2006.; D’Silva V. Widening for automata. PhD thesis, Institut fur Informatik, Universitaat Zurich; 2006.
[20] D’Silva V, Purandare M, Kroening D. Approximation refinement for interpolation-based model checking. In: VMCAI, 2008.; D’Silva V, Purandare M, Kroening D. Approximation refinement for interpolation-based model checking. In: VMCAI, 2008. · Zbl 1138.68444
[21] Feret, J., Static analysis of digital filters, (European symposium on programming (ESOP’04). Lecture notes in computer science, vol. 2986 (2004), Springer-Verlag) · Zbl 1126.68347
[22] Giacobazzi, R.; Ranzato, F., The reduced relative power operation on abstract domains, Theoretical Computer Science, 216, 1-2, 159-211 (1999) · Zbl 0914.68129
[23] Granger, P., Static analysis of linear congruence equalities among variables of a program, (International joint conference on theory and practice of software development (TAPSOFT’91). Lecture notes in computer science, vol. 464 (April 1991), Springer-Verlag), 169-192 · Zbl 0967.68509
[24] Granger, P., Improving the results of static analyses programs by local decreasing iteration, (Proceedings of FSTTCS. Lectures notes in computer science, vol. 652 (1992), Springer-Verlag), 68-79
[25] Van Hentenryck P, Cortesi A, Le Charlier B. Type analysis of prolog using type graphs. In: SIGPLAN conference on programming language design and implementation, 1994. p. 337-48.; Van Hentenryck P, Cortesi A, Le Charlier B. Type analysis of prolog using type graphs. In: SIGPLAN conference on programming language design and implementation, 1994. p. 337-48. · Zbl 0830.68029
[26] Rustan K, Leino M, Logozzo F. Using widenings to infer loop invariants inside an smt solver, or: A theorem prover as abstract domain. In: Workshop on invariant generation (WING 2007), Hagenberg, Austria, June 25-26, 2007.; Rustan K, Leino M, Logozzo F. Using widenings to infer loop invariants inside an smt solver, or: A theorem prover as abstract domain. In: Workshop on invariant generation (WING 2007), Hagenberg, Austria, June 25-26, 2007.
[27] Logozzo F, Fahndrich M. A weakly relational domain for the efficient validation of array accesses. In: 23th ACM symposium on applied computing (SAC 2008), Fortaleza, Brazil, 2008.; Logozzo F, Fahndrich M. A weakly relational domain for the efficient validation of array accesses. In: 23th ACM symposium on applied computing (SAC 2008), Fortaleza, Brazil, 2008. · Zbl 1197.68035
[28] Miné, A., The octagon abstract domain, (AST 2001 in WCRE 2001, IEEE (October 2001), IEEE CS Press), 310-319
[29] Miné A. Weakly relational numerical abstract domains. PhD thesis, École Polytechnique, Palaiseau, France, December \(2004 \langle\) http://www.di.ens.fr/mine/these/these-color.pdf \(\rangle \); Miné A. Weakly relational numerical abstract domains. PhD thesis, École Polytechnique, Palaiseau, France, December \(2004 \langle\) http://www.di.ens.fr/mine/these/these-color.pdf \(\rangle \)
[30] Miné, A., The octagon abstract domain, Higher-Order and Symbolic Computation, 19, 1, 31-100 (2006) · Zbl 1105.68069
[31] Nielson, F.; Nielson, R. H.; Hankin, C. L., Principles of program analysis (1999), Springer, [second printing] · Zbl 0932.68013
[32] Ramachandran, V.; Van Hentenryck, P.; Cortesi, A., Abstract domains for reordering CLP(RLin) programs, Journal of Logic Programming, 42, 3, 217-256 (2000) · Zbl 0952.68031
[33] Rival, X.; Mauborgne, L., The trace partitioning abstract domain, ACM Transactions on Programming Languages and Systems, 29, 5, 7-47 (2007)
[34] Venet, A., Abstract cofibered domains: application to the alias analysis of untyped programs, (Proceedings of the third international symposium on static analysis (SAS’96) (1996), Springer-Verlag), 366-382 · Zbl 1482.68098
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.