Abstract
We discuss the construction of proper widening operators on several weakly-relational numeric abstractions. Our proposal differs from previous ones in that we actually consider the semantic abstract domains, whose elements are geometric shapes, instead of the (more concrete) syntactic abstract domains of constraint networks and matrices. Since the closure by entailment operator preserves geometric shapes, but not their syntactic expressions, our widenings are immune from the divergence issues that could be faced by the previous approaches when interleaving the applications of widening and closure. The new widenings, which are variations of the standard widening for convex polyhedra defined by Cousot and Halbwachs, can be made as precise as the previous proposals working on the syntactic domains. The implementation of each new widening relies on the availability of an effective reduction procedure for the considered constraint description: we provide such an algorithm for the domain of octagonal shapes.
This work has been partly supported by MURST projects “Constraint Based Verification of Reactive Systems” and “AIDA — Abstract Interpretation: Design and Applications,” and by a Royal Society (UK) International Joint Project (ESEP) award.
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
Aho, A.V., Garey, M.R., Ullman, J.D.: The transitive reduction of a directed graph. SIAM Journal on Computing 1(2), 131–137 (1972)
Allen, J.F., Kautz, H.A.: A model of naive temporal reasoning. In: Formal Theories of the Commonsense World, Ablex, Norwood, NJ, pp. 251–268 (1985)
Bagnara, R.: Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Italy (1997)
Bagnara, R., Giacobazzi, R., Levi, G.: Static analysis of CLP programs over numeric domains. In: Proc. WSA 1992, Bordeaux. Bigre, vol. 81–82, pp. 43–50 (1992)
Bagnara, R., Giacobazzi, R., Levi, G.: An application of constraint propagation to data-flow analysis. In: Proc. CAIA 1993, Orlando, FL, pp. 270–276 (1993)
Bagnara, R., Hill, P.M., Mazzi, E., Zaffanella, E.: Widening operators for weakly-relational numeric abstractions. Quaderno 399, Dipartimento di Matematica, Univ. di Parma, Italy (2005), Available at, http://www.cs.unipr.it/Publications/
Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 337–354. Springer, Heidelberg (2003)
Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Science of Computer Programming (2005) (to appear)
Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 135–148. Springer, Heidelberg (2004)
Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library User’s Manual. Department of Mathematics, University of Parma, release 0.7 (2004)
Balasundaram, V., Kennedy, K.: A technique for summarizing data access and its use in parallelism enhancing transformations. In: Proc. PLDI 1989, OR. ACM SIGPLAN Notices, Portland, vol. 24(7), pp. 41–53 (1989)
Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)
Birkhoff, G.: Lattice Theory, 3rd edn. American Mathematical Society, Providence (1967)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., et al.: A static analyzer for large safety-critical software. In: Proc. PLDI 2003, San Diego, CA, pp. 196–207 (2003)
Clarisó, R., Cortadella, J.: The octahedron abstract domain. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 312–327. Springer, Heidelberg (2004)
Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proc. ISOP 1976, 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: Proc. POPL 1977, New York, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. POPL 1979, New York, pp. 269–282 (1979)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. POPL 1978, Tucson, AR, pp. 84–96 (1978)
Davis, E.: Constraint propagation with interval labels. Artificial Intelligence 32(3), 281–331 (1987)
Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)
Halbwachs, N.: Détermination Automatique de Relations Linéaires Vérifiées par les Variables d’un Programme. PhD thesis, Université de Grenoble, France (1979)
Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Form. Method Syst. Des. 11(2), 157–185 (1997)
Larsen, K., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: Compact data structure and state-space reduction. In: Proc. RTSS 1997, San Francisco, CA, pp. 14–24 (1997)
Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001)
Miné, A.: The octagon abstract domain. In: Proc. WCRE 2001, Stuttgart, pp. 310–319 (2001)
Miné, A.: A few graph-based relational numerical abstract domains. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 117–132. Springer, Heidelberg (2002)
Miné, A.: The Octagon Abstract Domain Library. École Normale Supérieure, Paris, France, release 0.9.6 (2002), Available at, http://www.di.ens.fr/~mine/oct/
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, Paris, France (2005)
Sankaranarayanan, S., Sipma, H., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005)
Shaham, R., Kolodner, E.K., Sagiv, S.: Automatic removal of array memory leaks in java. In: Watt, D.A. (ed.) CC 2000. LNCS, vol. 1781, pp. 50–66. Springer, Heidelberg (2000)
Simon, A., King, A., Howe, J.M.: Two variables per linear inequality as an abstract domain. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 71–89. Springer, Heidelberg (2003)
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
Bagnara, R., Hill, P.M., Mazzi, E., Zaffanella, E. (2005). Widening Operators for Weakly-Relational Numeric Abstractions. In: Hankin, C., Siveroni, I. (eds) Static Analysis. SAS 2005. Lecture Notes in Computer Science, vol 3672. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11547662_3
Download citation
DOI: https://doi.org/10.1007/11547662_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28584-7
Online ISBN: 978-3-540-31971-9
eBook Packages: Computer ScienceComputer Science (R0)