Advertisement

Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library

  • Roberto Bagnara
  • Elisa Ricci
  • Enea Zaffanella
  • Patricia M. Hill
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)

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.

Keywords

Closure Point Constraint System Convex Polyhedron Abstract Interpretation Minimal Form 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 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. 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. 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. 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. 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. 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. 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.zbMATHCrossRefGoogle Scholar
  9. 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.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 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.zbMATHCrossRefGoogle Scholar
  11. 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.CrossRefGoogle Scholar
  12. 12.
    P. Cousot, editor. Static Analysis: 8th International Symposium, SAS 2001, volume 2126 of Lecture Notes in Computer Science, Paris, 2001. Springer-Verlag, Berlin.zbMATHGoogle Scholar
  13. 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. 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. 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. 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. 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. 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. 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. 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. 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.CrossRefGoogle Scholar
  22. 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.zbMATHCrossRefGoogle Scholar
  23. 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. 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. 25.
    H. Le Verge. A note on Chernikova’s algorithm. Publication interne 635, IRISA, Campus de Beaulieu, Rennes, France, 1992.Google Scholar
  26. 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. 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. 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. 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. 30.
    W. Pugh. A practical algorithm for exact array dependence analysis. Communications of the ACM, 35(8):102–114, 1992.CrossRefGoogle Scholar
  31. 31.
    J. Stoer and C. Witzgall. Convexity and Optimization in Finite Dimensions I. Springer-Verlag, Berlin, 1970.Google Scholar
  32. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Roberto Bagnara
    • 1
  • Elisa Ricci
    • 1
  • Enea Zaffanella
    • 1
  • Patricia M. Hill
    • 2
  1. 1.Department of MathematicsUniversity of ParmaItaly
  2. 2.School of ComputingUniversity of LeedsUK

Personalised recommendations