{"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":1773234474215,"version":"3.50.1"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,5,30]],"date-time":"2009-05-30T00:00:00Z","timestamp":1243641600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2009,12]]},"DOI":"10.1007\/s10703-009-0073-1","type":"journal-article","created":{"date-parts":[[2009,5,29]],"date-time":"2009-05-29T17:14:03Z","timestamp":1243617243000},"page":"279-323","source":"Crossref","is-referenced-by-count":34,"title":["Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness"],"prefix":"10.1007","volume":"35","author":[{"given":"Roberto","family":"Bagnara","sequence":"first","affiliation":[]},{"given":"Patricia M.","family":"Hill","sequence":"additional","affiliation":[]},{"given":"Enea","family":"Zaffanella","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,5,30]]},"reference":[{"key":"73_CR1","first-page":"106","volume-title":"Proceedings of the Second International Symposium on Programming","author":"P Cousot","year":"1976","unstructured":"Cousot P, Cousot R (1976) Static determination of dynamic properties of programs. In: Robinet B (ed) Proceedings of the Second International Symposium on Programming, Paris, France. Dunod, Paris, pp 106\u2013130"},{"key":"73_CR2","first-page":"84","volume-title":"Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages","author":"P Cousot","year":"1978","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona. ACM, New York, pp 84\u201396"},{"key":"73_CR3","unstructured":"Bagnara R (1997) Data-flow analysis for constraint logic-based languages. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, Pisa, Italy. Printed as Report TD-1\/97"},{"key":"73_CR4","volume-title":"Actes \u201cWorkshop on Static Analysis\u201992\u201d","author":"R Bagnara","year":"1992","unstructured":"Bagnara R, Giacobazzi R, Levi G (1992) Static analysis of CLP programs over numeric domains. In: Billaud M, Cast\u00e9ran P, Corsini M, Musumbu K, Rauzy A (eds) Actes \u201cWorkshop on Static Analysis\u201992\u201d. Atelier Irisa, IRISA Campus de Beaulieu, Bordeaux. Bigre, vol 81\u201382, pp 43\u201350. Extended abstract"},{"key":"73_CR5","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1109\/CAIA.1993.366600","volume-title":"Proceedings of \u201cThe Ninth Conference on Artificial Intelligence for Applications\u201d","author":"R Bagnara","year":"1993","unstructured":"Bagnara R, Giacobazzi R, Levi G (1993) An application of constraint propagation to data-flow analysis. In: Proceedings of \u201cThe Ninth Conference on Artificial Intelligence for Applications\u201d, Orlando, Florida. IEEE Computer Society Press, Los Alamitos, pp 270\u2013276"},{"key":"73_CR6","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"Proceedings of the 2nd Symposium on Programs as Data Objects (PADO 2001)","author":"A Min\u00e9","year":"2001","unstructured":"Min\u00e9 A (2001) A new numerical abstract domain based on difference-bound matrices. In: Danvy O, Filinski A (eds) Proceedings of the 2nd Symposium on Programs as Data Objects (PADO 2001), Aarhus, Denmark. Lecture notes in computer science, vol 2053. Springer, Berlin, pp 155\u2013172"},{"key":"73_CR7","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-46423-9_4","volume-title":"Proceedings of the 9th International Conference on Compiler Construction (CC 2000)","author":"R Shaham","year":"2000","unstructured":"Shaham R, Kolodner EK, Sagiv S (2000) Automatic removal of array memory leaks in Java. In: Watt DA (ed) Proceedings of the 9th International Conference on Compiler Construction (CC 2000), Berlin, Germany. Lecture notes in computer science, vol 1781. Springer, Berlin, pp 50\u201366"},{"key":"73_CR8","doi-asserted-by":"crossref","first-page":"310","DOI":"10.1109\/WCRE.2001.957836","volume-title":"Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE\u201901)","author":"A Min\u00e9","year":"2001","unstructured":"Min\u00e9 A (2001) The octagon abstract domain. In: Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE\u201901), Stuttgart, Germany. IEEE Computer Society Press, Los Alamitos, pp 310\u2013319"},{"key":"73_CR9","series-title":"Lecture notes in computer science","first-page":"71","volume-title":"Logic Based Program Synthesis and Transformation, 12th International Workshop","author":"A Simon","year":"2002","unstructured":"Simon A, King A, Howe JM (2002) Two variables per linear inequality as an abstract domain. In: Leuschel M (ed) Logic Based Program Synthesis and Transformation, 12th International Workshop, Madrid, Spain. Lecture notes in computer science, vol 2664. Springer, Berlin, pp 71\u201389"},{"key":"73_CR10","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1007\/978-3-540-27864-1_23","volume-title":"Static Analysis: Proceedings of the 11th International Symposium","author":"R Claris\u00f3","year":"2004","unstructured":"Claris\u00f3 R, Cortadella J (2004) The octahedron abstract domain. In: Giacobazzi R (ed) Static Analysis: Proceedings of the 11th International Symposium, Verona, Italy. Lecture notes in computer science, vol 3148. Springer, Berlin, pp 312\u2013327"},{"key":"73_CR11","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"Verification, Model Checking and Abstract Interpretation: Proceedings of the 6th International Conference (VMCAI 2005)","author":"S Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan S, Sipma HB, Manna Z (2005) Scalable analysis of linear systems using mathematical programming. In: Cousot R (ed) Verification, Model Checking and Abstract Interpretation: Proceedings of the 6th International Conference (VMCAI 2005), Paris, France. Lecture notes in computer science, vol 3385. Springer, Berlin, pp 25\u201341"},{"key":"73_CR12","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/3-540-45789-5_11","volume-title":"Static Analysis: Proceedings of the 9th International Symposium","author":"A Min\u00e9","year":"2002","unstructured":"Min\u00e9 A (2002) A few graph-based relational numerical abstract domains. In: Hermenegildo MV, Puebla\u00a0G (eds) Static Analysis: Proceedings of the 9th International Symposium, Madrid, Spain. Lecture notes in computer science, vol 2477. Springer, Berlin, pp 117\u2013132"},{"key":"73_CR13","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/3-540-58601-6_92","volume-title":"Principles and Practice of Constraint Programming: Proceedings of the Second International Workshop","author":"J Jaffar","year":"1994","unstructured":"Jaffar J, Maher MJ, Stuckey PJ, Yap RHC (1994) Beyond finite domains. In: Borning A (ed) Principles and Practice of Constraint Programming: Proceedings of the Second International Workshop, Rosario, Orcas Island, Washington, USA. Lecture notes in computer science, vol 874. Springer, Berlin, pp 86\u201394"},{"issue":"1","key":"73_CR14","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1137\/0214016","volume":"14","author":"JC Lagarias","year":"1985","unstructured":"Lagarias JC (1985) The computational complexity of simultaneous Diophantine approximation problems. SIAM J Comput 14(1):196\u2013209","journal-title":"SIAM J Comput"},{"key":"73_CR15","series-title":"ACM SIGPLAN notices","first-page":"41","volume-title":"Proceedings of the ACM SIGPLAN\u201989 Conference on Programming Language Design and Implementation (PLDI)","author":"V Balasundaram","year":"1989","unstructured":"Balasundaram V, Kennedy K (1989) A technique for summarizing data access and its use in parallelism enhancing transformations. In: Knobe B (ed) Proceedings of the ACM SIGPLAN\u201989 Conference on Programming Language Design and Implementation (PLDI), Portland, Oregon, USA. ACM SIGPLAN notices, vol 24(7). ACM, New York, pp 41\u201353"},{"key":"73_CR16","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1007\/978-3-540-27813-9_36","volume-title":"Computer Aided Verification: Proceedings of the 16th International Conference","author":"T Ball","year":"2004","unstructured":"Ball T, Cook B, Lahiri SK, Zhang L (2004) Zapato: Automatic theorem proving for predicate abstraction refinement. In: Alur R, Peled D (eds) Computer Aided Verification: Proceedings of the 16th International Conference, Boston, MA, USA. Lecture notes in computer science, vol 3114. Springer, Berlin, pp 457\u2013461"},{"key":"73_CR17","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems, Proceedings of the 14th European Symposium on Programming","author":"P Cousot","year":"2005","unstructured":"Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2005) The Astr\u00e9e analyzer. In: Sagiv M (ed) Programming Languages and Systems, Proceedings of the 14th European Symposium on Programming, Edinburgh, UK. Lecture notes in computer science, vol 3444. Springer, Berlin, pp 21\u201330"},{"key":"73_CR18","unstructured":"Min\u00e9 A (2005) Weakly relational numerical abstract domains. PhD thesis, \u00c9cole Polytechnique, Paris, France"},{"key":"73_CR19","unstructured":"Halbwachs N (1979) 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"},{"key":"73_CR20","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/11547662_3","volume-title":"Static Analysis: Proceedings of the 12th International Symposium","author":"R Bagnara","year":"2005","unstructured":"Bagnara R, Hill PM, Mazzi E, Zaffanella E (2005) Widening operators for weakly-relational numeric abstractions. In: Hankin C, Siveroni I (eds) Static Analysis: Proceedings of the 12th International Symposium, London, UK. Lecture notes in computer science, vol 3672. Springer, Berlin, pp 3\u201318"},{"key":"73_CR21","doi-asserted-by":"crossref","unstructured":"Bagnara R, Hill PM, Mazzi E, Zaffanella E (2005) Widening operators for weakly-relational numeric abstractions. Quaderno 399, Dipartimento di Matematica, Universit\u00e0 di Parma, Italy. Available at http:\/\/www.cs.unipr.it\/Publications\/","DOI":"10.1007\/11547662_3"},{"key":"73_CR22","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1007\/978-3-540-78163-9_6","volume-title":"Verification, Model Checking and Abstract Interpretation: Proceedings of the 9th International Conference (VMCAI 2008)","author":"R Bagnara","year":"2008","unstructured":"Bagnara R, Hill PM, Zaffanella E (2008) An improved tight closure algorithm for integer octagonal constraints. In: Logozzo F, Peled D, Zuck L (eds) Verification, Model Checking and Abstract Interpretation: Proceedings of the 9th International Conference (VMCAI 2008), San Francisco, USA. Lecture notes in computer science, vol 4905. Springer, Berlin, pp 8\u201321"},{"key":"73_CR23","series-title":"Colloquium publications","volume-title":"Lattice theory","author":"G Birkhoff","year":"1967","unstructured":"Birkhoff G (1967) Lattice theory, 3rd edn. Colloquium publications, vol XXV. American Mathematical Society, Providence","edition":"3"},{"key":"73_CR24","first-page":"238","volume-title":"Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages","author":"P Cousot","year":"1977","unstructured":"Cousot P, Cousot R (1977) 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. ACM, New York, pp 238\u2013252"},{"key":"73_CR25","first-page":"269","volume-title":"Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages","author":"P Cousot","year":"1979","unstructured":"Cousot P, Cousot R (1979) Systematic design of program analysis frameworks. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages. ACM, New York, pp 269\u2013282"},{"key":"73_CR26","volume-title":"Introduction to algorithms","author":"TH Cormen","year":"1990","unstructured":"Cormen TH, Leiserson TE, Rivest RL (1990) Introduction to algorithms. The MIT Press, Cambridge"},{"key":"73_CR27","unstructured":"Pratt VR (1977) Two easy theories whose combination is hard. Memo sent to Nelson and Oppen concerning a preprint of their paper [49]"},{"key":"73_CR28","volume-title":"Dynamic programming","author":"R Bellman","year":"1957","unstructured":"Bellman R (1957) Dynamic programming. Princeton University Press, Princeton"},{"key":"73_CR29","first-page":"251","volume-title":"Formal theories of the commonsense world","author":"JF Allen","year":"1985","unstructured":"Allen JF, Kautz HA (1985) A model of naive temporal reasoning. In: Hobbs JR, Moore R (eds) Formal theories of the commonsense world. Ablex, Norwood, pp 251\u2013268"},{"issue":"3","key":"73_CR30","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/0004-3702(87)90091-9","volume":"32","author":"E Davis","year":"1987","unstructured":"Davis E (1987) Constraint propagation with interval labels. Artif Intell 32(3):281\u2013331","journal-title":"Artif Intell"},{"key":"73_CR31","series-title":"Lecture notes in computer science","first-page":"197","volume-title":"Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems","author":"DL Dill","year":"1989","unstructured":"Dill DL (1989) Timing assumptions and verification of finite-state concurrent systems. In: Sifakis J (ed) Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France. Lecture notes in computer science, vol 407. Springer, Berlin, pp 197\u2013212"},{"key":"73_CR32","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1109\/REAL.1997.641265","volume-title":"Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS\u201997)","author":"K Larsen","year":"1997","unstructured":"Larsen K, Larsson F, Pettersson P, Yi W (1997) Efficient verification of real-time systems: Compact data structure and state-space reduction. In: Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS\u201997). IEEE Computer Society Press, Los Alamitos, pp 14\u201324"},{"issue":"1\u20132","key":"73_CR33","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1016\/j.scico.2005.02.003","volume":"58","author":"R Bagnara","year":"2005","unstructured":"Bagnara R, Hill PM, Ricci E, Zaffanella E (2005) Precise widening operators for convex polyhedra. Sci Comput Program 58(1\u20132):28\u201356","journal-title":"Sci Comput Program"},{"issue":"2","key":"73_CR34","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1137\/0201008","volume":"1","author":"AV Aho","year":"1972","unstructured":"Aho AV, Garey MR, Ullman JD (1972) The transitive reduction of a directed graph. SIAM J Comput 1(2):131\u2013137","journal-title":"SIAM J Comput"},{"key":"73_CR35","series-title":"Lecture notes in computer science","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":"Halbwachs N, Proy YE, Raymond P (1994) Verification of linear hybrid systems by means of convex approximations. In: Le B (ed) Static Analysis: Proceedings of the 1st International Symposium, Namur, Belgium. Lecture notes in computer science, vol 864. Springer, Berlin, pp 223\u2013237"},{"issue":"2","key":"73_CR36","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N Halbwachs","year":"1997","unstructured":"Halbwachs N, Proy YE, Roumanoff P (1997) Verification of real-time systems using linear relation analysis. Form Methods Syst Des 11(2):157\u2013185","journal-title":"Form Methods Syst Des"},{"key":"73_CR37","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/3-540-36377-7_5","volume-title":"The essence of computation, complexity, analysis, transformation","author":"B Blanchet","year":"2002","unstructured":"Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2002) Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen T\u00c6, Schmidt DA, Sudborough IH (eds) The essence of computation, complexity, analysis, transformation. Lecture notes in computer science, vol 2566. Springer, Berlin, pp 85\u2013108. Essays Dedicated to Neil D\u00a0Jones [on occasion of his 60th birthday]"},{"key":"73_CR38","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1145\/781131.781153","volume-title":"Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI\u201903)","author":"B Blanchet","year":"2003","unstructured":"Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2003) A static analyzer for large safety-critical software. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI\u201903). ACM, New York, pp 196\u2013207"},{"key":"73_CR39","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-540-24725-8_2","volume-title":"Programming Languages and Systems: Proceedings of the 13th European Symposium on Programming","author":"A Min\u00e9","year":"2004","unstructured":"Min\u00e9 A (2004) Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt D (ed) Programming Languages and Systems: Proceedings of the 13th European Symposium on Programming, Barcelona, Spain. Lecture notes in computer science, vol 2986. Springer, Berlin, pp 3\u201317"},{"issue":"1\u20132","key":"73_CR40","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara R, Hill PM, Zaffanella E (2008) The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci Comput Program 72(1\u20132):3\u201321","journal-title":"Sci Comput Program"},{"issue":"4\/5","key":"73_CR41","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1007\/s10009-005-0215-8","volume":"8","author":"R Bagnara","year":"2006","unstructured":"Bagnara R, Hill PM, Zaffanella E (2006) Widening operators for powerset domains. Softw Tools Technol Transf 8(4\/5):449\u2013466. In the printed version of this article, all the figures have been improperly printed (rendering them useless). See [50]","journal-title":"Softw Tools Technol Transf"},{"key":"73_CR42","unstructured":"Min\u00e9 A (2002) The Octagon Abstract Domain Library. Semantics and Abstract Interpretation Computer Science Lab., \u00c9cole Normale Sup\u00e9rieure, Paris, France, release 0.9.6 edn. Available at http:\/\/www.di.ens.fr\/~mine\/oct\/"},{"key":"73_CR43","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1145\/996841.996869","volume-title":"Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation","author":"A Venet","year":"2004","unstructured":"Venet A, Brat G (2004) Precise and efficient static array bound checking for large embedded C programs. In: Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation (PLDI\u201904). ACM, New York, pp 231\u2013242"},{"key":"73_CR44","unstructured":"Harvey W, Stuckey PJ (1997) A unit two variable per inequality integer constraint solver for constraint logic programming. In Patel M (ed) ACSC\u201997: Proceedings of the 20th Australasian Computer Science Conference, vol\u00a019. Australian Computer Science Communications, pp 102\u2013111"},{"key":"73_CR45","doi-asserted-by":"crossref","unstructured":"Pugh W (1991) The Omega test: A fast and practical integer programming algorithm for dependence analysis. In Supercomputing 91","DOI":"10.1145\/125826.125848"},{"key":"73_CR46","series-title":"Lecture notes in computer science","first-page":"411","volume-title":"Languages and Compilers for Parallel Computing, 14th International Workshop","author":"R Seater","year":"2001","unstructured":"Seater R, Wonnacott D (2001) Polynomial time array dataflow analysis. In: Dietz HG (ed) Languages and Compilers for Parallel Computing, 14th International Workshop, Cumberland Falls, KY, USA. Lecture notes in computer science, vol 2624. Springer, Berlin, pp 411\u2013426"},{"key":"73_CR47","series-title":"Lecture notes in artificial intelligence","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/11559306_9","volume-title":"Frontiers of Combining Systems: Proceedings of the 5th International Workshop, FroCoS 2005","author":"SK Lahiri","year":"2005","unstructured":"Lahiri SK, Musuvathi M (2005) An efficient decision procedure for UTVPI constraints. In: Gramlich\u00a0B (ed) Frontiers of Combining Systems: Proceedings of the 5th International Workshop, FroCoS 2005, Vienna, Austria. Lecture notes in artificial intelligence, vol 3717. Springer, Berlin, pp 168\u2013183"},{"issue":"1","key":"73_CR48","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9 A (2006) The octagon abstract domain. Higher-Order Symb Comput 19(1):31\u2013100","journal-title":"Higher-Order Symb Comput"},{"key":"73_CR49","first-page":"114","volume-title":"Proceedings of the 18th Annual Symposium on Foundations of Computer Science","author":"G Nelson","year":"1977","unstructured":"Nelson G, Oppen DC (1977) Fast decision algorithms based on Union and Find. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS\u201977). IEEE Computer Society Press, Providence, pp 114\u2013119. The journal version of this paper is [51]"},{"issue":"3\/4","key":"73_CR50","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/s10009-007-0029-y","volume":"9","author":"R Bagnara","year":"2007","unstructured":"Bagnara R, Hill PM, Zaffanella E (2007) Widening operators for powerset domains. Softw Tools Technol Transf 9(3\/4):413\u2013414. Erratum to [41] containing all the figures properly printed","journal-title":"Softw Tools Technol Transf"},{"issue":"2","key":"73_CR51","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson G, Oppen DC (1980) Fast decision procedures based on congruence closure. J ACM 27(2):356\u2013364. An earlier version of this paper is [49]","journal-title":"J ACM"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0073-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-009-0073-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0073-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:50Z","timestamp":1559253950000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-009-0073-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,5,30]]},"references-count":51,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["73"],"URL":"https:\/\/doi.org\/10.1007\/s10703-009-0073-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,5,30]]}}}