{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T13:07:43Z","timestamp":1773234463673,"version":"3.50.1"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030341749","type":"print"},{"value":"9783030341756","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-34175-6_6","type":"book-chapter","created":{"date-parts":[[2019,11,17]],"date-time":"2019-11-17T19:01:29Z","timestamp":1574017289000},"page":"95-114","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Dissecting Widening: Separating Termination from Information"],"prefix":"10.1007","author":[{"given":"Graeme","family":"Gange","sequence":"first","affiliation":[]},{"given":"Jorge A.","family":"Navas","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Schachte","sequence":"additional","affiliation":[]},{"given":"Harald","family":"S\u00f8ndergaard","sequence":"additional","affiliation":[]},{"given":"Peter J.","family":"Stuckey","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,18]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-642-38856-9_4","volume-title":"Static Analysis","author":"G Amato","year":"2013","unstructured":"Amato, G., Scozzari, F.: Localizing widening and narrowing. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 25\u201342. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-38856-9_4"},{"key":"6_CR2","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1016\/j.scico.2005.02.003","volume":"58","author":"R Bagnara","year":"2005","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci. Comput. Program. 58, 28\u201356 (2005)","journal-title":"Sci. Comput. Program."},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Blanchet, B., et al.: A static analyzer for large safety-critical software. In: ACM Conference on Programming Language Design and Implementation, pp. 196\u2013207 (2003)","DOI":"10.1145\/781151.781153"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/BFb0039704","volume-title":"Formal Methods in Programming and Their Applications","author":"F Bourdoncle","year":"1993","unstructured":"Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Bj\u00f8rner, D., Broy, M., Pottosin, I.V. (eds.) Formal Methods in Programming and Their Applications. LNCS, vol. 735, pp. 128\u2013141. Springer, Heidelberg (1993). \nhttps:\/\/doi.org\/10.1007\/BFb0039704"},{"key":"6_CR5","doi-asserted-by":"publisher","first-page":"325","DOI":"10.4204\/EPTCS.129.19","volume":"129","author":"Agostino Cortesi","year":"2013","unstructured":"Cortesi, A., Costantini, G., Ferrara, P.: A survey on product operators in abstract interpretation. In: Banerjee, A., Danvy, O., Doh, K.-G., Hatcliff, J. (eds.) Semantics, Abstract Interpretation, and Reasoning about Programs. Electronic Proceedings in Theoretical Computer Science, vol. 129, pp. 325\u2013336 (2013)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"6_CR6","unstructured":"Cousot, P.: Semantic foundations of program analysis. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, pp. 303\u2013346. Prentice-Hall (1981)"},{"key":"6_CR7","unstructured":"Cousot, P.: Forward non-relational infinitary static analysis, 2005. Slide set 18 from MIT Course 16.399, Abstract Interpretation. \nhttp:\/\/www.mit.edu\/afs\/athena.mit.edu\/course\/16\/16.399\/www\/"},{"key":"6_CR8","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: Proceedings of the Fourth ACM Symposium Principles of Programming Languages, pp. 238\u2013252. ACM Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the Sixth ACM Symposium on Principles of Programming Languages, pp. 269\u2013282. ACM Press (1979)","DOI":"10.1145\/567752.567778"},{"issue":"4","key":"6_CR10","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Logic Comput. 2(4), 511\u2013547 (1992)","journal-title":"J. Logic Comput."},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Programming Language Implementation and Logic Programming","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269\u2013295. Springer, Heidelberg (1992). \nhttps:\/\/doi.org\/10.1007\/3-540-55844-6_142"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-77505-8_23","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"P Cousot","year":"2007","unstructured":"Cousot, P., et al.: Combination of abstractions in the ASTR\u00c9E static analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 272\u2013300. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-77505-8_23"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. In: Proceedings of the Fifth ACM Symposium on Principles of Programming Languages, pp. 84\u201397. ACM Press (1978)","DOI":"10.1145\/512760.512770"},{"key":"6_CR14","unstructured":"Crab: CoRnucopia of ABstractions: A language-agnostic library for abstract interpretation. \nhttps:\/\/github.com\/seahorn\/crab"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-642-38856-9_3","volume-title":"Static Analysis","author":"G Gange","year":"2013","unstructured":"Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: Abstract interpretation over non-lattice abstract domains. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 6\u201324. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-38856-9_3"},{"issue":"1","key":"6_CR16","first-page":"1:1","volume":"37","author":"G Gange","year":"2014","unstructured":"Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: Interval analysis and machine arithmetic: why signedness ignorance is bliss. ACM Trans. Program. Lang. Syst. 37(1), 1:1\u20131:35 (2014)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-662-49122-5_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G Gange","year":"2016","unstructured":"Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: An abstract domain of uninterpreted functions. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 85\u2013103. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49122-5_4"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/11817963_41","volume-title":"Computer Aided Verification","author":"D Gopan","year":"2006","unstructured":"Gopan, D., Reps, T.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 452\u2013466. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11817963_41"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-540-74061-2_22","volume-title":"Static Analysis","author":"D Gopan","year":"2007","unstructured":"Gopan, D., Reps, T.: Guided static analysis. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 349\u2013365. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-74061-2_22"},{"key":"6_CR20","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/j.entcs.2012.09.007","volume":"287","author":"E Goubault","year":"2012","unstructured":"Goubault, E., Gall, T.L., Putot, S.: An accurate join for zonotopes, preserving affine input\/output relations. Electr. Notes Theor. Comput. Sci. 287, 65\u201376 (2012)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-56287-7_95","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"P Granger","year":"1992","unstructured":"Granger, P.: Improving the results of static analyses of programs by local decreasing iterations. In: Shyamasundar, R. (ed.) FSTTCS 1992. LNCS, vol. 652, pp. 68\u201379. Springer, Heidelberg (1992). \nhttps:\/\/doi.org\/10.1007\/3-540-56287-7_95"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-642-33125-1_15","volume-title":"Static Analysis","author":"N Halbwachs","year":"2012","unstructured":"Halbwachs, N., Henry, J.: When the decreasing sequence fails. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 198\u2013213. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-33125-1_15"},{"key":"6_CR24","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. Formal Methods Syst. Des. 11, 157\u2013185 (1997)","journal-title":"Formal Methods Syst. Des."},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-642-24372-1_38","volume-title":"Automated Technology for Verification and Analysis","author":"L Lakhdar-Chaouch","year":"2011","unstructured":"Lakhdar-Chaouch, L., Jeannet, B., Girault, A.: Widening with thresholds for programs with complex control graphs. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 492\u2013502. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-24372-1_38"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-642-38088-4_12","volume-title":"NASA Formal Methods","author":"B Mihaila","year":"2013","unstructured":"Mihaila, B., Sepp, A., Simon, A.: Widening as abstract domain. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 170\u2013184. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-38088-4_12"},{"key":"6_CR27","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. 2053, pp. 155\u2013172. Springer, Heidelberg (2001). \nhttps:\/\/doi.org\/10.1007\/3-540-44978-7_10"},{"key":"6_CR28","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: Proceedings of the Workshop in Analysis, Slicing and Transformation, pp. 310\u2013319 (2001)"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/11924661_11","volume-title":"Programming Languages and Systems","author":"A Simon","year":"2006","unstructured":"Simon, A., King, A.: Widening polyhedra with landmarks. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol. 4279, pp. 166\u2013182. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11924661_11"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-34175-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,17]],"date-time":"2019-11-17T19:03:53Z","timestamp":1574017433000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-34175-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030341749","9783030341756"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-34175-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"18 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nusa Dua, Bali","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Indonesia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 December 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 December 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2019","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}