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
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
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.
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/.
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/.
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.
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.
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.
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/.
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.
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.
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.
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.
P. Cousot, editor. Static Analysis: 8th International Symposium, SAS 2001, volume 2126 of Lecture Notes in Computer Science, Paris, 2001. Springer-Verlag, Berlin.
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.
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.
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.
N. Dor, M. Rodeh, and S. Sagiv. Cleanness checking of string manipulations in C programs via integer analysis. In Cousot [12], pages 194–212.
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.
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.
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.
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.
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.
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.
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.
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.
H. Le Verge. A note on Chernikova’s algorithm. Publication interne 635, IRISA, Campus de Beaulieu, Rennes, France, 1992.
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].
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.
F. Mesnard and U. Neumerkel. Applying static analysis techniques for inferring termination conditions of logic programs. In Cousot [12], pages 93–110.
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.
W. Pugh. A practical algorithm for exact array dependence analysis. Communications of the ACM, 35(8):102–114, 1992.
J. Stoer and C. Witzgall. Convexity and Optimization in Finite Dimensions I. Springer-Verlag, Berlin, 1970.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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