{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:24:53Z","timestamp":1740122693613,"version":"3.37.3"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,12,9]],"date-time":"2017-12-09T00:00:00Z","timestamp":1512777600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/linproxy.fan.workers.dev:443\/http\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["306595"],"award-info":[{"award-number":["306595"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2018,12]]},"DOI":"10.1007\/s10703-017-0310-y","type":"journal-article","created":{"date-parts":[[2017,12,9]],"date-time":"2017-12-09T13:16:57Z","timestamp":1512825417000},"page":"384-406","update-policy":"https:\/\/linproxy.fan.workers.dev:443\/https\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Improving the results of program analysis by abstract interpretation beyond the decreasing sequence"],"prefix":"10.1007","volume":"53","author":[{"given":"R\u00e9my","family":"Boutonnet","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/linproxy.fan.workers.dev:443\/https\/orcid.org\/0000-0002-1426-7967","authenticated-orcid":false,"given":"Nicolas","family":"Halbwachs","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,12,9]]},"reference":[{"key":"310_CR1","doi-asserted-by":"crossref","unstructured":"Amato G, Scozzari F (2013) Localizing widening and narrowing. In: Static analysis international symposium, SAS 2013, Seattle, pp 25\u201342","DOI":"10.1007\/978-3-642-38856-9_4"},{"key":"310_CR2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.scico.2015.12.005","volume":"120","author":"G Amato","year":"2016","unstructured":"Amato G, Scozzari F, Seidl H, Apinis K, Vojdani V (2016) Efficiently intertwining widening and narrowing. Sci Comput Program 120:1\u201324","journal-title":"Sci Comput Program"},{"key":"310_CR3","doi-asserted-by":"crossref","unstructured":"Apinis K, Seidl H, Vojdani V (2012) Side-effecting constraint systems: a swiss army knife for program analysis. In: Asian symposium on programming languages and systems, APLAS 2012, Kyoto, Japan, pp 157\u2013172","DOI":"10.1007\/978-3-642-35182-2_12"},{"key":"310_CR4","doi-asserted-by":"crossref","unstructured":"Apinis K, Seidl H, Vojdani V (2013) How to combine widening and narrowing for non-monotonic systems of equations. In: Programming language design and implementation, PLDI 2013, Seattle, pp 377\u2013386","DOI":"10.1145\/2491956.2462190"},{"key":"310_CR5","doi-asserted-by":"crossref","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: Programming language design and implementation, PLDI 2003, San Diego, California, pp 196\u2013207","DOI":"10.1145\/781131.781153"},{"key":"310_CR6","doi-asserted-by":"crossref","unstructured":"Bardin S, Finkel A, Leroux J, Petrucci L (July 2003) Fast: fast acceleration of symbolic transition systems. In: Computer aided verification, CAV 2003, Boulder, Colorado, pp 118\u2013121","DOI":"10.1007\/978-3-540-45069-6_12"},{"key":"310_CR7","doi-asserted-by":"crossref","unstructured":"Bultan T, Gerber R, Pugh W (1997) Symbolic model checking of infinite state systems using Presburger arithmetic. In: Computer aided verification, CAV 1997, Haifa, Israel, pp 400\u2013411","DOI":"10.1007\/3-540-63166-6_39"},{"key":"310_CR8","doi-asserted-by":"crossref","unstructured":"Bagnara R, Hill PM, Ricci E, Zaffanella E (2003) Precise widening operators for convex polyhedra. In: Static analysis symposium, SAS 2003, San Diego, California, USA, pp 337\u2013354","DOI":"10.1007\/3-540-44898-5_19"},{"key":"310_CR9","unstructured":"Bourdoncle F (1993) Efficient chaotic iteration strategies with widenings. In: Bj\u00f8rner D, Broy M, Pottosin IV (eds) Formal methods in programming and their applications. Lecture notes in computer science, vol 735. Springer, Heidelberg"},{"key":"310_CR10","doi-asserted-by":"crossref","unstructured":"Bagnara R, Ricci E, Zaffanella E, Hill PM (2002) Possibly not closed convex polyhedra and the Parma Polyhedra Library. In: Static analysis symposium, SAS 2002, Madrid, Spain, pp 213\u2013229","DOI":"10.1007\/3-540-45789-5_17"},{"issue":"9","key":"310_CR11","doi-asserted-by":"crossref","first-page":"1293","DOI":"10.1109\/5.97299","volume":"79","author":"F Boussinot","year":"1991","unstructured":"Boussinot F, de Simone R (1991) The Esterel language. Proc IEEE 79(9):1293\u20131304","journal-title":"Proc IEEE"},{"key":"310_CR12","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1976) Static determination of dynamic properties of programs. In: 2nd international symposium on programming. Dunod, Paris","DOI":"10.1145\/390018.808314"},{"key":"310_CR13","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of programming languages, POPL 1977, Los Angeles, California, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"310_CR14","doi-asserted-by":"crossref","unstructured":"Costan A, Gaubert S, Goubault E, Martel M, Putot S (2005) A policy iteration algorithm for computing fixed points in static analysis of programs. In: Computer-aided verification, CAV 2005, Edinburgh, Scotland, pp 462\u2013475","DOI":"10.1007\/11513988_46"},{"key":"310_CR15","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Principles of programming languages, POPL 1978, Tucson, Arizona, pp 84\u201396","DOI":"10.1145\/512760.512770"},{"key":"310_CR16","doi-asserted-by":"crossref","unstructured":"Comon H, Jurski Y (June 1998) Multiple counters automata, safety analysis and Presburger arithmetic. In: Computer aided verification, CAV 1998, Vancouver, Canada, pp 268\u2013279","DOI":"10.1007\/BFb0028751"},{"key":"310_CR17","doi-asserted-by":"crossref","unstructured":"Cousot P (2015) Abstracting induction by extrapolation and interpolation. In: Verification. Model checking, and abstract interpretation, VMCAI 2015, Mumbai, India, pp 19\u201342","DOI":"10.1007\/978-3-662-46081-8_2"},{"issue":"1","key":"310_CR18","first-page":"24","volume":"37","author":"A Cortesi","year":"2011","unstructured":"Cortesi A, Zanioli M (2011) Widening and narrowing operators for abstract interpretation. Comput Lang Syst Struct 37(1):24\u201342","journal-title":"Comput Lang Syst Struct"},{"key":"310_CR19","doi-asserted-by":"crossref","unstructured":"Gulavani BS, Chakraborty S, Nori AV, Rajamani SK (2008) Automatically refining abstract interpretations. In: Tools and algorithms for construction and analysis of systems, TACAS 2008, Budapest, Hungary, pp 443\u2013458","DOI":"10.1007\/978-3-540-78800-3_33"},{"key":"310_CR20","doi-asserted-by":"crossref","unstructured":"Gonnord L, Halbwachs N (2006) Combining widening and acceleration in linear relation analysis. In: Static analysis symposium, SAS 2006, Seoul, Korea, pp 144\u2013160","DOI":"10.1007\/11823230_10"},{"key":"310_CR21","doi-asserted-by":"crossref","unstructured":"Goubault E (2001) Static analyses of the precision of floating-point operations. In: Static analysis symposium, SAS 2001, Paris, France, pp 234\u2013259","DOI":"10.1007\/3-540-47764-0_14"},{"key":"310_CR22","doi-asserted-by":"crossref","unstructured":"Gopan D, Reps T (2006) Lookahead widening. In: Computer aided verification, CAV 2006, Seattle, WA, pp 452\u2013466","DOI":"10.1007\/11817963_41"},{"key":"310_CR23","unstructured":"Gulavani BS, Rajamani SK (2006) Counterexample driven refinement for abstract interpretation. In: Tools and algorithms for construction and analysis of systems, TACAS 2006, Vienna, Austria, pp 474\u2013488"},{"key":"310_CR24","doi-asserted-by":"crossref","unstructured":"Gopan D, Reps TW (2007) Guided static analysis. In: Static analysis symposium, SAS 2007, Kongens Lyngby, Denmark, pp 349\u2013365","DOI":"10.1007\/978-3-540-74061-2_22"},{"key":"310_CR25","doi-asserted-by":"crossref","unstructured":"Gawlitza T, Seidl H (2007) Precise fixpoint computation through strategy iteration. In: European symposium on programming, ESOP 2007, Braga, Portugal, pp 300\u2013315","DOI":"10.1007\/978-3-540-71316-6_21"},{"key":"310_CR26","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.scico.2013.09.016","volume":"93","author":"L Gonnord","year":"2014","unstructured":"Gonnord L, Schrammel P (2014) Abstract acceleration in linear relation analysis. Sci Comput Program 93:125\u2013153","journal-title":"Sci Comput Program"},{"key":"310_CR27","doi-asserted-by":"crossref","unstructured":"Halbwachs N (1993) Delay analysis in synchronous programs. In: Computer-Aided Verification, CAV 1993, Elounda, Greece, pp 333\u2013346","DOI":"10.1007\/3-540-56922-7_28"},{"key":"310_CR28","doi-asserted-by":"crossref","unstructured":"Halbwachs N, Henry J (2012) When the decreasing sequence fails. In: Static analysis symposium, SAS 2012, Deauville, France, pp 198\u2013213","DOI":"10.1007\/978-3-642-33125-1_15"},{"key":"310_CR29","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1016\/j.entcs.2012.11.003","volume":"289","author":"J Henry","year":"2012","unstructured":"Henry J, Monniaux D, Moy M (2012) PAGAI: a path sensitive static analyzer. Electr Notes Theor Comput Sci 289:15\u201325","journal-title":"Electr Notes Theor Comput Sci"},{"issue":"2","key":"310_CR30","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":"310_CR31","doi-asserted-by":"crossref","unstructured":"Jeannet B, Min\u00e9 A (2009) Apron: a library of numerical abstract domains for static analysis. In: Computer aided verification, CAV 2009, Grenoble, France, pp 661\u2013667","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"310_CR32","doi-asserted-by":"crossref","unstructured":"Karpenkov E, Monniaux D, Wendler P (2016) Program analysis with local policy iteration. In: Verification. Model checking, and abstract interpretation, VMCAI 2016, St Petersburg, Florida, pp 127\u2013146","DOI":"10.1007\/978-3-662-49122-5_6"},{"key":"310_CR33","doi-asserted-by":"crossref","unstructured":"Lattner C, Adve V (2004) LLVM: a compilation framework for lifelong program analysis and transformation. In: Code generation and optimization, CGO 2004, Washington, DC, pp 75\u201386","DOI":"10.1109\/CGO.2004.1281665"},{"key":"310_CR34","doi-asserted-by":"crossref","unstructured":"Lakhdar-Chaouch L, Jeannet B, Girault A (2011) Widening with thresholds for programs with complex control graphs. In: Automated technology for verification and analysis, ATVA 2011, Taipei, Taiwan, pp 492\u2013502","DOI":"10.1007\/978-3-642-24372-1_38"},{"key":"310_CR35","doi-asserted-by":"crossref","unstructured":"Min\u00e9 A (2001) The Octagon abstract domain. In: Eighth working conference on reverse engineering, WCRE 2001, Stuttgart, Germany, pp 310\u2013319","DOI":"10.1109\/WCRE.2001.957836"},{"key":"310_CR36","unstructured":"Min\u00e9 A (2004) Weakly relational numerical abstract domains. PhD thesis, Ecole Polytechnique, Paris"},{"key":"310_CR37","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.entcs.2012.10.008","volume":"288","author":"D Monniaux","year":"2012","unstructured":"Monniaux D, Le Guen J (2012) Stratified static analysis based on variable dependencies. Electr Notes Theor Comput Sci 288:61\u201374","journal-title":"Electr Notes Theor Comput Sci"},{"key":"310_CR38","unstructured":"Putot S, Goubault E, Martel M (2003) Static analysis-based validation of floating-point computations. In: Numerical software with result verification, international Dagstuhl seminar. LNCS 2991, Springer, Berlin, pp 306\u2013313"},{"issue":"4","key":"310_CR39","doi-asserted-by":"crossref","first-page":"645","DOI":"10.1137\/0208051","volume":"8","author":"A Shamir","year":"1979","unstructured":"Shamir A (1979) A linear time algorithm for finding minimum cutsets in reducible graphs. SIAM J Comput 8(4):645\u2013655","journal-title":"SIAM J Comput"},{"key":"310_CR40","doi-asserted-by":"crossref","unstructured":"Simon A, King A (2006) Widening polyhedra with landmarks. In: Asian symposium on programming languages and systems, APLAS 2006, Sydney, Australia, pp 166\u2013182","DOI":"10.1007\/11924661_11"},{"key":"310_CR41","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S, Sipma H, Manna Z (2004) Constraint-based linear relations analysis. In: Static analysis symposium, SAS 2004, Verona, Italy, pp 53\u201368","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"310_CR42","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S, Sipma H, Manna Z (2005) Scalable analysis of linear systems using mathematical programming. In: Verification, model-checking, and abstract intepretation, VMCAI 2005, Paris, France, pp 25\u201341","DOI":"10.1007\/978-3-540-30579-8_2"},{"key":"310_CR43","doi-asserted-by":"crossref","unstructured":"Su Z, Wagner D (2004) A class of polynomially solvable range constraints for interval analysis without widenings and narrowings. In: Tools and algorithms for construction and analysis of systems, TACAS 2004, Barcelona, Spain, pp 280\u2013295","DOI":"10.1007\/978-3-540-24730-2_23"},{"key":"310_CR44","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"RE Tarjan","year":"1972","unstructured":"Tarjan RE (1972) Depth-first search and linear graph algorithms. SIAM J Comput 1:146\u2013160","journal-title":"SIAM J Comput"},{"key":"310_CR45","doi-asserted-by":"crossref","unstructured":"Wolper P, Boigelot B (1998) Verifying systems with infinite but regular state spaces. In: Computer-aided verification, CAV\u201998, Vancouver, Canada, pp 88\u201397","DOI":"10.1007\/BFb0028736"},{"key":"310_CR46","doi-asserted-by":"crossref","unstructured":"Wang C, Yang Z, Gupta A, Ivan\u010di\u0107 F (2007) Using counterexamples for improving the precision of reachability computation with polyhedra. In: Computer-aided verification, CAV 2007, Berlin, Germany, pp 352\u2013365","DOI":"10.1007\/978-3-540-73368-3_40"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/linproxy.fan.workers.dev:443\/http\/link.springer.com\/article\/10.1007\/s10703-017-0310-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/linproxy.fan.workers.dev:443\/http\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0310-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/linproxy.fan.workers.dev:443\/http\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0310-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,10]],"date-time":"2022-08-10T04:15:05Z","timestamp":1660104905000},"score":1,"resource":{"primary":{"URL":"https:\/\/linproxy.fan.workers.dev:443\/http\/link.springer.com\/10.1007\/s10703-017-0310-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,9]]},"references-count":46,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,12]]}},"alternative-id":["310"],"URL":"https:\/\/linproxy.fan.workers.dev:443\/https\/doi.org\/10.1007\/s10703-017-0310-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2017,12,9]]}}}