{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:21Z","timestamp":1760202561822},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540403258"},{"type":"electronic","value":"9783540448983"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44898-5_19","type":"book-chapter","created":{"date-parts":[[2007,11,11]],"date-time":"2007-11-11T03:21:25Z","timestamp":1194751285000},"page":"337-354","source":"Crossref","is-referenced-by-count":33,"title":["Precise Widening Operators for Convex Polyhedra"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Bagnara","sequence":"first","affiliation":[]},{"given":"Patricia M.","family":"Hill","sequence":"additional","affiliation":[]},{"given":"Elisa","family":"Ricci","sequence":"additional","affiliation":[]},{"given":"Enea","family":"Zaffanella","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"key":"19_CR1","series-title":"Printed as Report","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, March 1997. Printed as Report TD-1\/97."},{"key":"19_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 http:\/\/www.cs.unipr.it\/ppl\/.","edition":"release 0.4 edi"},{"key":"19_CR3","volume-title":"Precise widening operators for convex polyhedra","author":"R. Bagnara","year":"2003","unstructured":"R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. Quaderno 312, Dipartimento di Matematica, Universit\u00e0 di Parma, Italy, 2003. Available at http:\/\/www.cs.unipr.it\/Publications\/."},{"key":"19_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/3-540-45789-5_17","volume-title":"Static Analysis: Proceedings of the 9th International Symposium","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. In M. V. Hermenegildo and G. Puebla, editors, Static Analysis: Proceedings of the 9th International Symposium, volume 2477 of Lecture Notes in Computer Science, pages 213\u2013229, Madrid, Spain, 2002. Springer-Verlag, Berlin."},{"key":"19_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 Program 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 Program 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":"19_CR6","volume-title":"Polyhedral Domains for Abstract Interpretation in Logic Programming","author":"P. M. Benoy","year":"2002","unstructured":"P. M. Benoy. Polyhedral Domains for Abstract Interpretation in Logic Programming. PhD thesis, Computing Laboratory, University of Kent, Canterbury, Kent, UK, January 2002."},{"key":"19_CR7","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":"19_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/BFb0039704","volume-title":"Proceedings of the International Conference on \u201cFormal Methods in Programming and Their Applications\u201d","author":"F. Bourdoncle","year":"1993","unstructured":"F. Bourdoncle. Efficient chaotic iteration strategies with widenings. In D. Bj\u00f8rner, M. Broy, and I. V. Pottosin, editors, Proceedings of the International Conference on \u201cFormal Methods in Programming and Their Applications\u201d, volume 735 of Lecture Notes in Computer Science, pages 128\u2013141, Academgorodok, Novosibirsk, Russia, 1993. Springer-Verlag, Berlin."},{"key":"19_CR9","unstructured":"F. Bourdoncle. S\u00e9mantiques des langages imp\u00e9ratifs d\u2019ordre sup\u00e9rieur et interpr\u00e9tation abstraite. PRL Research Report 22, DEC Paris Research Laboratory, 1993."},{"issue":"4","key":"19_CR10","doi-asserted-by":"publisher","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1999","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems, 21(4):747\u2013789, 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"19_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Tools and Algorithms for Construction and Analysis of Systems, 7th International Conference, 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, Tools and Algorithms for Construction and Analysis of Systems, 7th International Conference, TACAS 2001, volume 2031 of Lecture Notes in Computer Science, pages 67\u201381, Genova, Italy, 2001. Springer-Verlag, Berlin."},{"key":"19_CR12","volume-title":"Introduction to Algorithms","author":"T. H. Cormen","year":"1990","unstructured":"T. H. Cormen, T. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. The MIT Press, Cambridge, Mass., 1990."},{"key":"19_CR13","first-page":"303","volume-title":"Program Flow Analysis: Theory and Applications","author":"P. Cousot","year":"1981","unstructured":"P. Cousot. Semantic foundations of program analysis. In S. S. Muchnick and N. D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pages 303\u2013342. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, 1981."},{"key":"19_CR14","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, France, 2001. Springer-Verlag, Berlin."},{"key":"19_CR15","first-page":"106","volume-title":"Proceedings of the Second International Symposium on Programming","author":"P. Cousot","year":"1976","unstructured":"P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In B. Robinet, editor, Proceedings of the Second International Symposium on Programming, pages 106\u2013130. Dunod, Paris, France, 1976."},{"key":"19_CR16","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, New York, 1977. ACM Press.","DOI":"10.1145\/512950.512973"},{"issue":"4","key":"19_CR17","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511\u2013547, 1992.","journal-title":"Journal of Logic and Computation"},{"key":"19_CR18","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":"19_CR19","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":"19_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS\u201999","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno and A. Podelski. Model checking in CLP. In R. Cleaveland, editor, Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS\u201999, volume 1579 of Lecture Notes in Computer Science, pages 223\u2013239, Amsterdam, The Netherlands, 1999. Springer-Verlag, Berlin."},{"issue":"8","key":"19_CR21","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465\u2013476, 1979.","journal-title":"Communications of the ACM"},{"key":"19_CR22","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 [14], pages 194\u2013212."},{"key":"19_CR23","volume-title":"D\u00e9termination Automatique de Relations Lin\u00e9aires V\u00e9rifi\u00e9es par les Variables d\u2019un Programme","author":"N. Halbwachs","year":"1979","unstructured":"N. Halbwachs. D\u00e9termination Automatique de Relations Lin\u00e9aires V\u00e9rifi\u00e9es par les Variables d\u2019un Programme. Th\u00e8se de 3\u00e8me cycle d\u2019informatique, Universit\u00e9 scientifique et m\u00e9dicale de Grenoble, Grenoble, France, March 1979."},{"key":"19_CR24","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":"19_CR25","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":"19_CR26","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"},{"key":"19_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-60472-3_13","volume-title":"Hybrid Systems II","author":"T. A. Henzinger","year":"1995","unstructured":"T. A. Henzinger and P.-H. Ho. A note on abstract interpretation strategies for hybrid automata. In P. J. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors, Hybrid Systems II, volume 999 of Lecture Notes in Computer Science, pages 252\u2013264. Springer-Verlag, Berlin, 1995."},{"issue":"1+2","key":"19_CR28","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":"19_CR29","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":"19_CR30","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, B. 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":"19_CR31","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 [14], pages 93\u2013110."},{"issue":"8","key":"19_CR32","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"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44898-5_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T03:51:40Z","timestamp":1551066700000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44898-5_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540403258","9783540448983"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-44898-5_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}