Skip to main content
SpringerLink
Log in

Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library

  • Conference paper
  • First Online:
Book cover Static Analysis (SAS 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2477))

Included in the following conference series:

Abstract

The domain of convex polyhedra is employed in several systems for the analysis and verification of hardware and software components. Current applications span imperative, functional and logic languages, synchronous languages and synchronization protocols, real-time and hybrid systems. Since the seminal work of P. Cousot and N. Halbwachs, convex polyhedra have thus played an important role in the formal methods community and several critical tasks rely on their software implementations. Despite this, existing libraries for the manipulation of convex polyhedra are still research prototypes and suffer from limitations that make their usage problematic, especially in critical applications. Furthermore, there is inadequate support for polyhedra that are not necessarily closed (NNC), i.e., polyhedra that are described by systems of constraints where strict inequalities are allowed to occur. This paper presents the Parma Polyhedra Library, a new, robust and complete implementation of NNC convex polyhedra, concentrating on the distinctive features of the library and on the novel theoretical underpinnings.

This work has been partly supported by MURST projects “Abstract Interpretation, type systems and control-flow analysis” and “Aggregate- and number-reasoning for computing: from decision algorithms to constraint programming with multisets, sets, and maps” and by EPSRC grant GR/R53401/01.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Bagnara. Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Pisa, Italy, 1997. Printed as Report TD-1/97.

    Google Scholar 

  2. R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. The Parma Polyhedra Library User’s Manual, Department of Mathematics, University of Parma, Parma, Italy, release 0.4 edition, July 2002. Available at http://www.cs.unipr.it/ppl/.

    Google Scholar 

  3. R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Possibly not closed convex polyhedra and the Parma Polyhedra Library. Quaderno 286, Dipartimento di Matematica, Università di Parma, Italy, 2002. See also [4]. Available at http://www.cs.unipr.it/Publications/.

    Google Scholar 

  4. R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Errata for technical report “Quaderno 286”. Available at http://www.cs.unipr.it/Publications/, 2002.

  5. F. Benoy and A. King. Inferring argument size relationships with CLP(R). In J. P. Gallagher, editor, Logic Programming Synthesis and Transformation: Proceedings of the 6th International Workshop, volume 1207 of Lecture Notes in Computer Science, pages 204–223, Stockholm, Sweden, 1997. Springer-Verlag, Berlin.

    Google Scholar 

  6. F. Besson, T. P. Jensen, and J.-P. Talpin. Polyhedral analysis for synchronous languages. In A. Cortesi and G. Filé, editors, Static Analysis: Proceedings of the 6th International Symposium, volume 1694 of Lecture Notes in Computer Science, pages 51–68, Venice, Italy, 1999. Springer-Verlag, Berlin.

    Google Scholar 

  7. N. S. Bjørner, A. Browne, M. Colón, B. Finkbeiner, Z. Manna, M. Pichora, H. B. Sipma, and T. E. Uribe. STeP: The Stanford Temporal Prover (Educational Release) User’s Manual. Computer Science Department, Stanford University, Stanford, California, version 1.4-α edition, July 1998. Available at http://www-step.stanford.edu/.

    Google Scholar 

  8. N. V. Chernikova. Algorithm for finding a general formula for the non-negative solutions of system of linear equations. U.S.S.R. Computational Mathematics and Mathematical Physics, 4(4):151–158, 1964.

    Article  MATH  Google Scholar 

  9. N. V. Chernikova. Algorithm for finding a general formula for the non-negative solutions of system of linear inequalities. U.S.S.R. Computational Mathematics and Mathematical Physics, 5(2):228–233, 1965.

    Article  MATH  MathSciNet  Google Scholar 

  10. N. V. Chernikova. Algorithm for discovering the set of all solutions of a linear programming problem. U.S.S.R. Computational Mathematics and Mathematical Physics, 8(6):282–293, 1968.

    Article  MATH  Google Scholar 

  11. M. A. Colón and H. B. Sipma. Synthesis of linear ranking functions. In T. Margaria and W. Yi, editors, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), volume 2031 of Lecture Notes in Computer Science, pages 67–81, Genova, Italy, 2001. Springer-Verlag, Berlin.

    Chapter  Google Scholar 

  12. P. Cousot, editor. Static Analysis: 8th International Symposium, SAS 2001, volume 2126 of Lecture Notes in Computer Science, Paris, 2001. Springer-Verlag, Berlin.

    MATH  Google Scholar 

  13. P. Cousot and R. Cousot. 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, pages 238–252, 1977.

    Google Scholar 

  14. P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, volume 631 of Lecture Notes in Computer Science, pages 269–295, Leuven, Belgium, 1992. Springer-Verlag, Berlin.

    Google Scholar 

  15. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 84–96, Tucson, Arizona, 1978. ACM Press.

    Google Scholar 

  16. N. Dor, M. Rodeh, and S. Sagiv. Cleanness checking of string manipulations in C programs via integer analysis. In Cousot [12], pages 194–212.

    Google Scholar 

  17. K. Fukuda and A. Prodon. Double description method revisited. In M. Deza, R. Euler, and Y. Manoussakis, editors, Combinatorics and Computer Science, 8th Franco-Japanese and 4th Franco-Chinese Conference, Brest, France, July 3–5, 1995, Selected Papers, volume 1120 of Lecture Notes in Computer Science, pages 91–111. Springer-Verlag, Berlin, 1996.

    Google Scholar 

  18. N. Halbwachs. Delay analysis in synchronous programs. In C. Courcoubetis, editor, Computer Aided Verification: Proceedings of the 5th International Conference, volume 697 of Lecture Notes in Computer Science, pages 333–346, Elounda, Greece, 1993. Springer-Verlag, Berlin.

    Google Scholar 

  19. N. Halbwachs, A. Kerbrat, and Y.-E. Proy. POLyhedra INtegrated Environment. Verimag, France, version 1.0 of POLINE edition, September 1995. Documentation taken from source code.

    Google Scholar 

  20. N. Halbwachs, Y.-E. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations. In B. Le Charlier, editor, Static Analysis: Proceedings of the 1st International Symposium, volume 864 of Lecture Notes in Computer Science, pages 223–237, Namur, Belgium, 1994. Springer-Verlag, Berlin.

    Google Scholar 

  21. N. Halbwachs, Y.-E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157–185, 1997.

    Article  Google Scholar 

  22. T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1(1+2):110–122, 1997.

    Article  MATH  Google Scholar 

  23. T. A. Henzinger, J. Preussig, and H. Wong-Toi. Some lessons from the hytech experience. In Proceedings of the 40th Annual Conference on Decision and Control, pages 2887–2892. IEEE Computer Society Press, 2001.

    Google Scholar 

  24. B. Jeannet. Convex Polyhedra Library, release 1.1.3c edition, March 2002. Documentation of the “New Polka” library available at http://www.irisa.fr/prive/Bertrand.Jeannet/newpolka.html.

  25. H. Le Verge. A note on Chernikova’s algorithm. Publication interne 635, IRISA, Campus de Beaulieu, Rennes, France, 1992.

    Google Scholar 

  26. V. Loechner. PolyLib: A library for manipulating parameterized polyhedra. Available at http://icps.u-strasbg.fr~loechner/polylib/, March 1999. Declares itself to be a continuation of [32].

  27. Z. Manna, N. S. Bjørner, A. Browne, M. Colón, Finkbeiner, M. Pichora, H. B. Sipma, and T. E. Uribe. An update on STeP: Deductive-algorithmic verification of reactive systems. In R. Berghammer and Y. Lakhnech, editors, Tool Support for System Specification, Development and Verification, Advances in Computing Sciences. Springer-Verlag, Berlin, 1999.

    Google Scholar 

  28. F. Mesnard and U. Neumerkel. Applying static analysis techniques for inferring termination conditions of logic programs. In Cousot [12], pages 93–110.

    Google Scholar 

  29. T. S. Motzkin, H. Raiffa, G. L. Thompson, and R. M. Thrall. The double description method. In H. W. Kuhn and A. W. Tucker, editors, Contributions to the Theory of Games-Volume II, number 28 in Annals of Mathematics Studies, pages 51–73. Princeton University Press, Princeton, New Jersey, 1953.

    Google Scholar 

  30. W. Pugh. A practical algorithm for exact array dependence analysis. Communications of the ACM, 35(8):102–114, 1992.

    Article  Google Scholar 

  31. J. Stoer and C. Witzgall. Convexity and Optimization in Finite Dimensions I. Springer-Verlag, Berlin, 1970.

    Google Scholar 

  32. D. K. Wilde. 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.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics, University of Parma, Italy

    Roberto Bagnara, Elisa Ricci & Enea Zaffanella

  2. School of Computing, University of Leeds, UK

    Patricia M. Hill

Authors
  1. Roberto Bagnara
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Elisa Ricci
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Enea Zaffanella
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Patricia M. Hill
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science Facultad de Informática, Technical University of Madrid, Campus de Montegancedo, 28660, Boadilla del Monte, Madrid, Spain

    Manuel V. Hermenegildo  & Germán Puebla  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M. (2002). Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library. In: Hermenegildo, M.V., Puebla, G. (eds) Static Analysis. SAS 2002. Lecture Notes in Computer Science, vol 2477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45789-5_17

Download citation

  • DOI: https://doi.org/10.1007/3-540-45789-5_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44235-6

  • Online ISBN: 978-3-540-45789-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation