{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T04:38:03Z","timestamp":1776487083837,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540442356","type":"print"},{"value":"9783540457893","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45789-5_17","type":"book-chapter","created":{"date-parts":[[2007,8,11]],"date-time":"2007-08-11T13:50:10Z","timestamp":1186840210000},"page":"213-229","source":"Crossref","is-referenced-by-count":65,"title":["Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Bagnara","sequence":"first","affiliation":[]},{"given":"Elisa","family":"Ricci","sequence":"additional","affiliation":[]},{"given":"Enea","family":"Zaffanella","sequence":"additional","affiliation":[]},{"given":"Patricia M.","family":"Hill","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,5]]},"reference":[{"key":"17_CR1","series-title":"PhD thesis","volume-title":"Data-Flow Analysis for Constraint Logic-Based Languages","author":"R. Bagnara","year":"1997","unstructured":"R. Bagnara. Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, Pisa, Italy, 1997. Printed as Report TD-1\/97."},{"key":"17_CR2","volume-title":"The Parma Polyhedra Library User\u2019s Manual","author":"R. Bagnara","year":"2002","unstructured":"R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. The Parma Polyhedra Library User\u2019s Manual, Department of Mathematics, University of Parma, Parma, Italy, release 0.4 edition, July 2002. Available at \n                  http:\/\/www.cs.unipr.it\/ppl\/\n                  \n                ."},{"key":"17_CR3","volume-title":"Possibly not closed convex polyhedra and the Parma Polyhedra Library. Quaderno 286","author":"R. Bagnara","year":"2002","unstructured":"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\u00e0 di Parma, Italy, 2002. See also [4]. Available at \n                  http:\/\/www.cs.unipr.it\/Publications\/\n                  \n                ."},{"key":"17_CR4","unstructured":"R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Errata for technical report \u201cQuaderno 286\u201d. Available at \n                  http:\/\/www.cs.unipr.it\/Publications\/\n                  \n                , 2002."},{"key":"17_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/3-540-62718-9_12","volume-title":"Logic Programming Synthesis and Transformation: Proceedings of the 6th International Workshop","author":"F. Benoy","year":"1997","unstructured":"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\u2013223, Stockholm, Sweden, 1997. Springer-Verlag, Berlin."},{"key":"17_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/3-540-48294-6_4","volume-title":"Static Analysis: Proceedings of the 6th International Symposium","author":"F. Besson","year":"1999","unstructured":"F. Besson, T. P. Jensen, and J.-P. Talpin. Polyhedral analysis for synchronous languages. In A. Cortesi and G. Fil\u00e9, editors, Static Analysis: Proceedings of the 6th International Symposium, volume 1694 of Lecture Notes in Computer Science, pages 51\u201368, Venice, Italy, 1999. Springer-Verlag, Berlin."},{"key":"17_CR7","volume-title":"STeP: The Stanford Temporal Prover (Educational Release) User\u2019s Manual","author":"N. S. Bj\u00f8rner","year":"1998","unstructured":"N. S. Bj\u00f8rner, A. Browne, M. Col\u00f3n, B. Finkbeiner, Z. Manna, M. Pichora, H. B. Sipma, and T. E. Uribe. STeP: The Stanford Temporal Prover (Educational Release) User\u2019s Manual. Computer Science Department, Stanford University, Stanford, California, version 1.4-\u03b1 edition, July 1998. Available at \n                  http:\/\/www-step.stanford.edu\/."},{"issue":"4","key":"17_CR8","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/0041-5553(64)90009-6","volume":"4","author":"N. V. Chernikova","year":"1964","unstructured":"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\u2013158, 1964.","journal-title":"U.S.S.R. Computational Mathematics and Mathematical Physics"},{"issue":"2","key":"17_CR9","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1016\/0041-5553(65)90045-5","volume":"5","author":"N. V. Chernikova","year":"1965","unstructured":"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\u2013233, 1965.","journal-title":"U.S.S.R. Computational Mathematics and Mathematical Physics"},{"issue":"6","key":"17_CR10","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1016\/0041-5553(68)90115-8","volume":"8","author":"N. V. Chernikova","year":"1968","unstructured":"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\u2013293, 1968.","journal-title":"U.S.S.R. Computational Mathematics and Mathematical Physics"},{"key":"17_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001)","author":"M. A. Col\u00f3n","year":"2001","unstructured":"M. A. Col\u00f3n 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\u201381, Genova, Italy, 2001. Springer-Verlag, Berlin."},{"key":"17_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Static Analysis: 8th International Symposium, SAS 2001","year":"2001","unstructured":"P. Cousot, editor. Static Analysis: 8th International Symposium, SAS 2001, volume 2126 of Lecture Notes in Computer Science, Paris, 2001. Springer-Verlag, Berlin."},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"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\u2013252, 1977.","DOI":"10.1145\/512950.512973"},{"key":"17_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming","author":"P. Cousot","year":"1992","unstructured":"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\u2013295, Leuven, Belgium, 1992. Springer-Verlag, Berlin."},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"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\u201396, Tucson, Arizona, 1978. ACM Press.","DOI":"10.1145\/512760.512770"},{"key":"17_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1007\/3-540-47764-0_12","volume-title":"Static Analysis: 8th International Symposium, SAS 2001","author":"N. Dor","year":"2001","unstructured":"N. Dor, M. Rodeh, and S. Sagiv. Cleanness checking of string manipulations in C programs via integer analysis. In Cousot [12], pages 194\u2013212."},{"key":"17_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/3-540-61576-8_77","volume-title":"Combinatorics and Computer Science, 8th Franco-Japanese and 4th Franco-Chinese Conference, Brest, France, July 3\u20135, 1995, Selected Papers","author":"K. Fukuda","year":"1996","unstructured":"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\u20135, 1995, Selected Papers, volume 1120 of Lecture Notes in Computer Science, pages 91\u2013111. Springer-Verlag, Berlin, 1996."},{"key":"17_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/3-540-56922-7_28","volume-title":"Computer Aided Verification: Proceedings of the 5th International Conference","author":"N. Halbwachs","year":"1993","unstructured":"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\u2013346, Elounda, Greece, 1993. Springer-Verlag, Berlin."},{"key":"17_CR19","unstructured":"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."},{"key":"17_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/3-540-58485-4_43","volume-title":"Static Analysis: Proceedings of the 1st International Symposium","author":"N. Halbwachs","year":"1994","unstructured":"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\u2013237, Namur, Belgium, 1994. Springer-Verlag, Berlin."},{"issue":"2","key":"17_CR21","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"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\u2013185, 1997.","journal-title":"Formal Methods in System Design"},{"issue":"1+2","key":"17_CR22","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T. A. Henzinger","year":"1997","unstructured":"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\u2013122, 1997.","journal-title":"Software Tools for Technology Transfer"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"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\u20132892. IEEE Computer Society Press, 2001.","DOI":"10.1109\/CDC.2001.980714"},{"key":"17_CR24","unstructured":"B. Jeannet. Convex Polyhedra Library, release 1.1.3c edition, March 2002. Documentation of the \u201cNew Polka\u201d library available at \n                  http:\/\/www.irisa.fr\/prive\/Bertrand.Jeannet\/newpolka.html\n                  \n                ."},{"key":"17_CR25","unstructured":"H. Le Verge. A note on Chernikova\u2019s algorithm. Publication interne 635, IRISA, Campus de Beaulieu, Rennes, France, 1992."},{"key":"17_CR26","unstructured":"V. Loechner. PolyLib: A library for manipulating parameterized polyhedra. Available at \n                  http:\/\/icps.u-strasbg.fr~loechner\/polylib\/\n                  \n                , March 1999. Declares itself to be a continuation of [32]."},{"key":"17_CR27","series-title":"Advances in Computing Sciences","volume-title":"Tool Support for System Specification, Development and Verification","author":"Z. Manna","year":"1999","unstructured":"Z. Manna, N. S. Bj\u00f8rner, A. Browne, M. Col\u00f3n, 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."},{"key":"17_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/3-540-47764-0_6","volume-title":"Static Analysis: 8th International Symposium, SAS 2001","author":"F. Mesnard","year":"2001","unstructured":"F. Mesnard and U. Neumerkel. Applying static analysis techniques for inferring termination conditions of logic programs. In Cousot [12], pages 93\u2013110."},{"key":"17_CR29","series-title":"Annals of Mathematics Studies","first-page":"51","volume-title":"Contributions to the Theory of Games-Volume II","author":"T. S. Motzkin","year":"1953","unstructured":"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\u201373. Princeton University Press, Princeton, New Jersey, 1953."},{"issue":"8","key":"17_CR30","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"35","author":"W. Pugh","year":"1992","unstructured":"W. Pugh. A practical algorithm for exact array dependence analysis. Communications of the ACM, 35(8):102\u2013114, 1992.","journal-title":"Communications of the ACM"},{"key":"17_CR31","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-46216-0","volume-title":"Convexity and Optimization in Finite Dimensions I","author":"J. Stoer","year":"1970","unstructured":"J. Stoer and C. Witzgall. Convexity and Optimization in Finite Dimensions I. Springer-Verlag, Berlin, 1970."},{"key":"17_CR32","volume-title":"Master\u2019s thesis","author":"D. K. Wilde","year":"1993","unstructured":"D. K. Wilde. A library for doing polyhedral operations. Master\u2019s thesis, Oregon State University, Corvallis, Oregon, December 1993. Also published as IRISA Publication interne 785, Rennes, France, 1993."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45789-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T11:37:21Z","timestamp":1550749041000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45789-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540442356","9783540457893"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-45789-5_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}