{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,15]],"date-time":"2025-04-15T17:01:02Z","timestamp":1744736462718},"reference-count":41,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"funder":[{"name":"French Agence Nationale de la Recherche","award":["ANR-11-INSE-014"],"award-info":[{"award-number":["ANR-11-INSE-014"]}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Computer Languages, Systems & Structures"],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1016\/j.cl.2015.10.001","type":"journal-article","created":{"date-parts":[[2015,10,27]],"date-time":"2015-10-27T00:00:43Z","timestamp":1445904043000},"page":"77-103","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":3,"special_numbering":"P1","title":["Inference of ranking functions for proving temporal properties by abstract interpretation"],"prefix":"10.1016","volume":"47","author":[{"given":"Caterina","family":"Urban","sequence":"first","affiliation":[]},{"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"2","key":"10.1016\/j.cl.2015.10.001_bib1","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","article-title":"Proving the correctness of multiprocess programs","volume":"3","author":"Lamport","year":"1977","journal-title":"IEEE Trans Softw Eng"},{"key":"10.1016\/j.cl.2015.10.001_bib2","doi-asserted-by":"crossref","unstructured":"Manna Z, Pnueli A, A hierarchy of temporal properties. In: PODC, 1990. p. 377\u2013410.","DOI":"10.1145\/93385.93442"},{"key":"10.1016\/j.cl.2015.10.001_bib3","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: POPL, 1977. p. 238\u2013252.","DOI":"10.1145\/512950.512973"},{"key":"10.1016\/j.cl.2015.10.001_bib4","doi-asserted-by":"crossref","unstructured":"Bertrane J, Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, et al. Static analysis and verification of aerospace software by abstract interpretation. In: AIAA, 2010. p. 1\u201338.","DOI":"10.2514\/6.2010-3385"},{"key":"10.1016\/j.cl.2015.10.001_bib5","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R. An abstract interpretation framework for termination. In: POPL, 2012. p. 245\u2013258.","DOI":"10.1145\/2103656.2103687"},{"key":"10.1016\/j.cl.2015.10.001_bib6","doi-asserted-by":"crossref","unstructured":"Urban C. The abstract domain of segmented ranking functions. In: SAS, 2013. p. 43\u201362.","DOI":"10.1007\/978-3-642-38856-9_5"},{"key":"10.1016\/j.cl.2015.10.001_bib7","doi-asserted-by":"crossref","unstructured":"Urban C, Min\u00e9 A. An abstract domain to infer ordinal-valued ranking functions. In: ESOP, 2014. p. 412\u2013431.","DOI":"10.1007\/978-3-642-54833-8_22"},{"key":"10.1016\/j.cl.2015.10.001_bib8","doi-asserted-by":"crossref","unstructured":"Urban C, Min\u00e9 A. A decision tree abstract domain for proving conditional termination. In: SAS, 2014. p. 302\u2013318.","DOI":"10.1007\/978-3-319-10936-7_19"},{"key":"10.1016\/j.cl.2015.10.001_bib9","series-title":"Fairness","author":"Francez","year":"1986"},{"key":"10.1016\/j.cl.2015.10.001_bib11","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/S1571-0661(05)80168-9","article-title":"Constructive design of a hierarchy of semantics of a transition system by abstract interpretation","volume":"6","author":"Cousot","year":"1997","journal-title":"Electron Not Theor Comput Sci"},{"key":"10.1016\/j.cl.2015.10.001_bib12","unstructured":"Turing A. Checking a large routine. In: Report of a conference on high speed automatic calculating machines, 1949. p. 67\u201369."},{"key":"10.1016\/j.cl.2015.10.001_bib13","doi-asserted-by":"crossref","unstructured":"Floyd RW. Assigning meanings to programs. In: Proceedings of symposium on applied mathematics, vol. 19, 1967. p. 19\u201332.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"10.1016\/j.cl.2015.10.001_bib14","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R. Higher order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection, and PER analysis). In: ICCL, 1994. p. 95\u2013112.","DOI":"10.1109\/ICCL.1994.288389"},{"key":"10.1016\/j.cl.2015.10.001_bib15","first-page":"59","article-title":"Fixpoint induction and proofs of program properties","volume":"5","author":"Park","year":"1969","journal-title":"Mach Intell"},{"key":"10.1016\/j.cl.2015.10.001_bib16","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R. Static determination of dynamic properties of programs. In: Symposium on programming, 1976. p. 106\u2013130.","DOI":"10.1145\/800022.808314"},{"key":"10.1016\/j.cl.2015.10.001_bib17","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N. Automatic discovery of linear restraints among variables of a program. In: POPL, 1978. p. 84\u201396.","DOI":"10.1145\/512760.512770"},{"issue":"1","key":"10.1016\/j.cl.2015.10.001_bib18","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","article-title":"The octagon abstract domain","volume":"19","author":"Min\u00e9","year":"2006","journal-title":"Higher-Order Symbol Comput"},{"key":"10.1016\/j.cl.2015.10.001_bib19","doi-asserted-by":"crossref","unstructured":"Chakarov A, Sankaranarayanan S. Expectation invariants for probabilistic program loops as fixed points. In: SAS, 2014. p. 85\u2013100.","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"10.1016\/j.cl.2015.10.001_bib20","doi-asserted-by":"crossref","unstructured":"Min\u00e9 A. Inferring sufficient conditions with backward polyhedral under-approximations. Electron Not Theor Comput Sci 2012;287:89-100","DOI":"10.1016\/j.entcs.2012.09.009"},{"key":"10.1016\/j.cl.2015.10.001_bib21","doi-asserted-by":"crossref","unstructured":"Jeannet B, Min\u00e9 A. Apron: a library of numerical abstract domains for static analysis. In: CAV, 2009. p. 661\u2013667.","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"10.1016\/j.cl.2015.10.001_bib22","doi-asserted-by":"crossref","unstructured":"Bourdoncle F. Efficient chaotic iteration strategies with widenings. In: FMPA, 1993. p. 128\u2013141.","DOI":"10.1007\/BFb0039704"},{"key":"10.1016\/j.cl.2015.10.001_bib23","doi-asserted-by":"crossref","unstructured":"D\u05f3Silva V, Urban C. Conflict-driven conditional termination. In: CAV (II), 2015. p. 271\u2013286.","DOI":"10.1007\/978-3-319-21668-3_16"},{"issue":"2","key":"10.1016\/j.cl.2015.10.001_bib24","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1016\/S1571-0661(04)80410-9","article-title":"Liveness checking as safety checking","volume":"66","author":"Biere","year":"2002","journal-title":"Electron Not Theor Comput Sci"},{"key":"10.1016\/j.cl.2015.10.001_bib25","unstructured":"Bradley AR, Somenzi F, Hassan Z, Zhang Y. An incremental approach to model checking progress properties. In: FMCAD, 2011. p. 144\u2013153."},{"key":"10.1016\/j.cl.2015.10.001_bib26","doi-asserted-by":"crossref","unstructured":"Podelski A, Rybalchenko A. Transition predicate abstraction and fair termination. In: POPL, 2005. p. 132\u2013144.","DOI":"10.1145\/1040305.1040317"},{"key":"10.1016\/j.cl.2015.10.001_bib27","doi-asserted-by":"crossref","unstructured":"Podelski A, Rybalchenko A. Transition invariants. In: LICS, 2004. p. 32\u201341.","DOI":"10.1109\/LICS.2004.1319598"},{"issue":"1\u20132","key":"10.1016\/j.cl.2015.10.001_bib28","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0168-0072(91)90066-U","article-title":"Verification of concurrent programs: the automata-theoretic framework","volume":"51","author":"Vardi","year":"1991","journal-title":"Ann Pure Appl Logic"},{"key":"10.1016\/j.cl.2015.10.001_bib29","doi-asserted-by":"crossref","unstructured":"Cook B, Gotsman A, Podelski A, Rybalchenko A, Vardi MY. Proving that programs eventually do something good. In: POPL, 2007. p. 265\u2013276.","DOI":"10.1145\/1190216.1190257"},{"key":"10.1016\/j.cl.2015.10.001_bib30","doi-asserted-by":"crossref","unstructured":"Lee CS, Jones ND, Ben-Amram AM. The size-change principle for program termination. In: POPL, 2001. p. 81\u201392.","DOI":"10.1145\/360204.360210"},{"key":"10.1016\/j.cl.2015.10.001_bib31","doi-asserted-by":"crossref","unstructured":"Berdine J, Chawdhary A, Cook B, Distefano D, O\u05f3Hearn PW. Variance analyses from invariance analyses. In: POPL, 2007. p. 211\u2013224.","DOI":"10.1145\/1190215.1190249"},{"key":"10.1016\/j.cl.2015.10.001_bib32","doi-asserted-by":"crossref","unstructured":"Mass\u00e9 D. Property checking driven abstract interpretation-based static analysis. In: VMCAI, 2003. p. 56\u201369.","DOI":"10.1007\/3-540-36384-X_8"},{"key":"10.1016\/j.cl.2015.10.001_bib33","doi-asserted-by":"crossref","unstructured":"Mass\u00e9 D. Abstract domains for property checking driven analysis of temporal properties. In: AMAST, 2004. p. 349\u2013363.","DOI":"10.1007\/978-3-540-27815-3_28"},{"key":"10.1016\/j.cl.2015.10.001_bib34","doi-asserted-by":"crossref","unstructured":"Beyene TA, Popeea C, Rybalchenko A. Solving existentially quantified horn clauses. In: CAV, 2013. p. 869\u2013882.","DOI":"10.1007\/978-3-642-39799-8_61"},{"key":"10.1016\/j.cl.2015.10.001_bib35","doi-asserted-by":"crossref","unstructured":"Cook B, Koskinen E. Reasoning about nondeterminism in programs. In: PLDI, 2013. p. 219\u2013230.","DOI":"10.1145\/2491956.2491969"},{"issue":"5","key":"10.1016\/j.cl.2015.10.001_bib36","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","article-title":"Counterexample-guided abstraction refinement for symbolic model checking","volume":"50","author":"Clarke","year":"2003","journal-title":"J ACM"},{"key":"10.1016\/j.cl.2015.10.001_bib37","doi-asserted-by":"crossref","unstructured":"Cook B, Khlaaf H, Piterman N. Faster temporal reasoning for infinite-state programs. In: FMCAD, 2014. p. 75\u201382.","DOI":"10.1109\/FMCAD.2014.6987598"},{"key":"10.1016\/j.cl.2015.10.001_bib38","doi-asserted-by":"crossref","unstructured":"Cook B, Khlaaf H, Piterman N. On automation of CTL* verification for infinite-state systems. In: CAV (I), 2015. p. 13\u201329.","DOI":"10.1007\/978-3-319-21690-4_2"},{"key":"10.1016\/j.cl.2015.10.001_bib39","doi-asserted-by":"crossref","unstructured":"Cook B, Gulwani S, Lev-Ami T, Rybalchenko A, Sagiv M. Proving conditional termination. In: CAV, 2008. p. 328\u2013340.","DOI":"10.1007\/978-3-540-70545-1_32"},{"key":"10.1016\/j.cl.2015.10.001_bib40","doi-asserted-by":"crossref","unstructured":"Ganty P, Genaim S. Proving termination starting from the end. In: CAV, 2013. p. 397\u2013412.","DOI":"10.1007\/978-3-642-39799-8_27"},{"key":"10.1016\/j.cl.2015.10.001_bib41","doi-asserted-by":"crossref","unstructured":"Mass\u00e9 D. Policy iteration-based conditional termination and ranking functions. In: VMCAI, 2014. p. 453\u2013471.","DOI":"10.1007\/978-3-642-54013-4_25"},{"key":"10.1016\/j.cl.2015.10.001_bib10","doi-asserted-by":"crossref","unstructured":"Urban C, Min\u00e9 A. Proving guarantee and recurrence temporal properties by abstract interpretation. In: VMCAI, 2015. p. 190\u2013208.","DOI":"10.1007\/978-3-662-46081-8_11"}],"container-title":["Computer Languages, Systems & Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1477842415000743?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1477842415000743?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,9,1]],"date-time":"2019-09-01T00:25:00Z","timestamp":1567297500000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1477842415000743"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":41,"alternative-id":["S1477842415000743"],"URL":"https:\/\/doi.org\/10.1016\/j.cl.2015.10.001","relation":{},"ISSN":["1477-8424"],"issn-type":[{"value":"1477-8424","type":"print"}],"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Inference of ranking functions for proving temporal properties by abstract interpretation","name":"articletitle","label":"Article Title"},{"value":"Computer Languages, Systems & Structures","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.cl.2015.10.001","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2015 Elsevier Ltd. All rights reserved.","name":"copyright","label":"Copyright"}]}}