{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T13:07:54Z","timestamp":1773234474619,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540285847","type":"print"},{"value":"9783540319719","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11547662_3","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T10:36:20Z","timestamp":1127817380000},"page":"3-18","source":"Crossref","is-referenced-by-count":13,"title":["Widening Operators for Weakly-Relational Numeric Abstractions"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Bagnara","sequence":"first","affiliation":[]},{"given":"Patricia M.","family":"Hill","sequence":"additional","affiliation":[]},{"given":"Elena","family":"Mazzi","sequence":"additional","affiliation":[]},{"given":"Enea","family":"Zaffanella","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"3_CR1","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1137\/0201008","volume":"1","author":"A.V. Aho","year":"1972","unstructured":"Aho, A.V., Garey, M.R., Ullman, J.D.: The transitive reduction of a directed graph. SIAM Journal on Computing\u00a01(2), 131\u2013137 (1972)","journal-title":"SIAM Journal on Computing"},{"key":"3_CR2","unstructured":"Allen, J.F., Kautz, H.A.: A model of naive temporal reasoning. In: Formal Theories of the Commonsense World, Ablex, Norwood, NJ, pp. 251\u2013268 (1985)"},{"key":"3_CR3","unstructured":"Bagnara, R.: Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, Italy (1997)"},{"key":"3_CR4","unstructured":"Bagnara, R., Giacobazzi, R., Levi, G.: Static analysis of CLP programs over numeric domains. In: Proc. WSA 1992, Bordeaux. Bigre, vol.\u00a081\u201382, pp. 43\u201350 (1992)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Bagnara, R., Giacobazzi, R., Levi, G.: An application of constraint propagation to data-flow analysis. In: Proc. CAIA 1993, Orlando, FL, pp. 270\u2013276 (1993)","DOI":"10.1109\/CAIA.1993.366600"},{"key":"3_CR6","unstructured":"Bagnara, R., Hill, P.M., Mazzi, E., Zaffanella, E.: Widening operators for weakly-relational numeric abstractions. Quaderno 399, Dipartimento di Matematica, Univ. di Parma, Italy (2005), Available at, http:\/\/www.cs.unipr.it\/Publications\/"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-44898-5_19","volume-title":"Static Analysis","author":"R. Bagnara","year":"2003","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 337\u2013354. Springer, Heidelberg (2003)"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Science of Computer Programming (2005) (to appear)","DOI":"10.1016\/j.scico.2005.02.003"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-24622-0_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Bagnara","year":"2004","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 135\u2013148. Springer, Heidelberg (2004)"},{"key":"3_CR10","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library User\u2019s Manual. Department of Mathematics, University of Parma, release 0.7 (2004)"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Balasundaram, V., Kennedy, K.: A technique for summarizing data access and its use in parallelism enhancing transformations. In: Proc. PLDI 1989, OR. ACM SIGPLAN Notices, Portland, vol.\u00a024(7), pp. 41\u201353 (1989)","DOI":"10.1145\/73141.74822"},{"key":"3_CR12","volume-title":"Dynamic Programming","author":"R. Bellman","year":"1957","unstructured":"Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)"},{"key":"3_CR13","volume-title":"Lattice Theory","author":"G. Birkhoff","year":"1967","unstructured":"Birkhoff, G.: Lattice Theory, 3rd edn. American Mathematical Society, Providence (1967)","edition":"3"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., et al.: A static analyzer for large safety-critical software. In: Proc. PLDI 2003, San Diego, CA, pp. 196\u2013207 (2003)","DOI":"10.1145\/781131.781153"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-540-27864-1_23","volume-title":"Static Analysis","author":"R. Claris\u00f3","year":"2004","unstructured":"Claris\u00f3, R., Cortadella, J.: The octahedron abstract domain. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 312\u2013327. Springer, Heidelberg (2004)"},{"key":"3_CR16","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proc. ISOP 1976, Paris, France, pp. 106\u2013130 (1976)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. POPL 1977, New York, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. POPL 1979, New York, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. POPL 1978, Tucson, AR, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"issue":"3","key":"3_CR20","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/0004-3702(87)90091-9","volume":"32","author":"E. Davis","year":"1987","unstructured":"Davis, E.: Constraint propagation with interval labels. Artificial Intelligence\u00a032(3), 281\u2013331 (1987)","journal-title":"Artificial Intelligence"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D.L. Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 197\u2013212. Springer, Heidelberg (1990)"},{"key":"3_CR22","unstructured":"Halbwachs, N.: D\u00e9termination Automatique de Relations Lin\u00e9aires V\u00e9rifi\u00e9es par les Variables d\u2019un Programme. PhD thesis, Universit\u00e9 de Grenoble, France (1979)"},{"issue":"2","key":"3_CR23","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Form. Method Syst. Des.\u00a011(2), 157\u2013185 (1997)","journal-title":"Form. Method Syst. Des."},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Larsen, K., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: Compact data structure and state-space reduction. In: Proc. RTSS 1997, San Francisco, CA, pp. 14\u201324 (1997)","DOI":"10.1109\/REAL.1997.641265"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"Programs as Data Objects","author":"A. Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol.\u00a02053, pp. 155\u2013172. Springer, Heidelberg (2001)"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: Proc. WCRE 2001, Stuttgart, pp. 310\u2013319 (2001)","DOI":"10.1109\/WCRE.2001.957836"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-45789-5_11","volume-title":"Static Analysis","author":"A. Min\u00e9","year":"2002","unstructured":"Min\u00e9, A.: A few graph-based relational numerical abstract domains. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 117\u2013132. Springer, Heidelberg (2002)"},{"key":"3_CR28","unstructured":"Min\u00e9, A.: The Octagon Abstract Domain Library. \u00c9cole Normale Sup\u00e9rieure, Paris, France, release 0.9.6 (2002), Available at, http:\/\/www.di.ens.fr\/~mine\/oct\/"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-24725-8_2","volume-title":"Programming Languages and Systems","author":"A. Min\u00e9","year":"2004","unstructured":"Min\u00e9, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 3\u201317. Springer, Heidelberg (2004)"},{"key":"3_CR30","unstructured":"Min\u00e9, A.: Weakly Relational Numerical Abstract Domains. PhD thesis, \u00c9cole Polytechnique, Paris, France (2005)"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 25\u201341. Springer, Heidelberg (2005)"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-46423-9_4","volume-title":"Compiler Construction","author":"R. Shaham","year":"2000","unstructured":"Shaham, R., Kolodner, E.K., Sagiv, S.: Automatic removal of array memory leaks in java. In: Watt, D.A. (ed.) CC 2000. LNCS, vol.\u00a01781, pp. 50\u201366. Springer, Heidelberg (2000)"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/3-540-45013-0_7","volume-title":"Logic Based Program Synthesis and Transformation","author":"A. Simon","year":"2003","unstructured":"Simon, A., King, A., Howe, J.M.: Two variables per linear inequality as an abstract domain. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol.\u00a02664, pp. 71\u201389. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11547662_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T02:57:54Z","timestamp":1619492274000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11547662_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540285847","9783540319719"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/11547662_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}