Abstract
The finite powerset construction upgrades an abstract domain by allowing for the representation of finite disjunctions of its elements. In this paper we define two generic widening operators for the finite powerset abstract domain. Both widenings are obtained by lifting any widening operator defined on the base-level abstract domain and are parametric with respect to the specification of a few additional operators. We illustrate the proposed techniques by instantiating our widenings on powersets of convex polyhedra, a domain for which no non-trivial widening operator was previously known.
This work has been partly supported by MURST projects “Aggregate- and Number-Reasoning for Computing: from Decision Algorithms to Constraint Programming with Multisets, Sets, and Maps” and “Constraint Based Verification of Reactive Systems.”
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abramsky, S., Jung, A.: Domain theory. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 3, ch. 1, pp. 1–168. Clarendon Press, Oxford (1994)
Bagnara, R.: A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages. Science of Computer Programming 30(1–2), 119–155 (1998)
Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: The Parma Polyhedra Library User’s Manual. Department of Mathematics, University of Parma, Parma, Italy, release 0.5 edition (April 2003), Available at http://www.cs.unipr.it/ppl/
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., Zaffanella, E.: Widening operators for powerset domains. Quaderno, Dipartimento di Matematica, Università di Parma, Italy (2003) (to appear)
Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the Parma Polyhedra Library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 213–229. Springer, Heidelberg (2002)
Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems 21(4), 747–789 (1999)
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)
Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Robinet, B. (ed.) Proceedings of the Second International Symposium on Programming, 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: Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, pp. 238–252. ACM Press, New York (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages, pp. 269–282. ACM Press, New York (1979)
Cousot, P., Cousot, R.: Abstract interpretation and applications to logic programs. Journal of Logic Programming 13(2&3), 103–179 (1992)
Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–547 (1992)
Cousot, P., Cousot, R.: Comparing the Galois connection and widening/ narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pp. 84–96. ACM Press, Tucson (1978)
Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 223–239. Springer, Heidelberg (1999)
Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM 22(8), 465–476 (1979)
Filé, G., Ranzato, F.: The powerset operator on abstract interpretations. Theoretical Computer Science 222, 77–111 (1999)
Halbwachs, N.: Détermination Automatique de Relations Linéaires Vérifiées par les Variables d’un Programme. Thèse de 3ème cycle d’informatique, Université scientifique et médicale de Grenoble, Grenoble, France (March 1979)
Halbwachs, N.: Delay analysis in synchronous programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 333–346. Springer, Heidelberg (1993)
Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11(2), 157–185 (1997)
Holzbaur, C.: OFAI clp(q,r) manual, edition 1.3.3. Technical Report TR-95-09, Austrian Research Institute for Artificial Intelligence, Vienna (1995)
Kelly, W., Maslov, V., Pugh, W., Rosser, E., Shpeisman, T., Wonnacott, D.: The Omega library interface guide. Technical Report CS-TR-3445, Department of Computer Science, University of Maryland, College Park, MD, USA (1995)
Le Verge, H.: A note on Chernikova’s algorithm. Publication interne 635, IRISA, Campus de Beaulieu, Rennes, France (1992)
Loechner, V.: PolyLib: A library for manipulating parameterized polyhedra (March 1999), Available at http://icps.u-strasbg.fr/~loechner/polylib/ ; Declares itself to be a continuation of [28]
Pugh, W.: A practical algorithm for exact array dependence analysis. Communications of the ACM 35(8), 102–114 (1992)
Srivastava, D.: Subsumption and indexing in constraint query languages with linear arithmetic constraints. Annals of Mathematics and Artificial Intelligence 8(3-4), 315–343 (1993)
Wilde, D.K.: A library for doing polyhedral operations. Master’s thesis, Oregon State University, Corvallis, Oregon (December 1993); Also published as IRISA Publication interne 785, Rennes, France (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bagnara, R., Hill, P.M., Zaffanella, E. (2004). Widening Operators for Powerset Domains. In: Steffen, B., Levi, G. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2004. Lecture Notes in Computer Science, vol 2937. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24622-0_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-24622-0_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20803-7
Online ISBN: 978-3-540-24622-0
eBook Packages: Springer Book Archive