{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T21:48:55Z","timestamp":1648676935027},"reference-count":15,"publisher":"Elsevier BV","issue":"11","license":[{"start":{"date-parts":[[2015,11,1]],"date-time":"2015-11-01T00:00:00Z","timestamp":1446336000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Information Processing Letters"],"published-print":{"date-parts":[[2015,11]]},"DOI":"10.1016\/j.ipl.2015.05.012","type":"journal-article","created":{"date-parts":[[2015,5,29]],"date-time":"2015-05-29T04:54:02Z","timestamp":1432875242000},"page":"882-885","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":1,"title":["A second-order formulation of non-termination"],"prefix":"10.1016","volume":"115","author":[{"given":"Fred","family":"Mesnard","sequence":"first","affiliation":[]},{"given":"\u00c9tienne","family":"Payet","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"3","key":"10.1016\/j.ipl.2015.05.012_br0010","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-7(3:4)2011","article-title":"Monotonicity constraints for termination in the integer domain","volume":"7","author":"Ben-Amram","year":"2011","journal-title":"Log. Methods Comput. Sci."},{"issue":"3","key":"10.1016\/j.ipl.2015.05.012_br0020","article-title":"Deciding conditional termination","volume":"10","author":"Bozga","year":"2014","journal-title":"Log. Methods Comput. Sci."},{"key":"10.1016\/j.ipl.2015.05.012_br0030","series-title":"Proc. of the 6th International Conference on Verification, Model Checking and Abstract Interpretation","first-page":"113","article-title":"Termination of polynomial programs","volume":"vol. 3385","author":"Bradley","year":"2005"},{"key":"10.1016\/j.ipl.2015.05.012_br0040","series-title":"Proc. of the 18th International Conference on Computer Aided Verification","first-page":"372","article-title":"Termination of integer linear programs","volume":"vol. 4144","author":"Braverman","year":"2006"},{"key":"10.1016\/j.ipl.2015.05.012_br0050","series-title":"Proc. of the 1960 International Congress on Logic, Methodology and Philosophy of Science","first-page":"1","article-title":"On a decision method in restricted second-order arithmetic","author":"B\u00fcchi","year":"1962"},{"key":"10.1016\/j.ipl.2015.05.012_br0060","series-title":"Proc. of the 21st International Conference on Logic Programming","first-page":"326","article-title":"Testing for termination with monotonicity constraints","volume":"vol. 3668","author":"Codish","year":"2005"},{"key":"10.1016\/j.ipl.2015.05.012_br0070","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0004-3702(89)90012-X","article-title":"On the existence of nonterminating queries for a restricted class of Prolog-clauses","volume":"41","author":"De Schreye","year":"1989","journal-title":"Artif. Intell."},{"key":"10.1016\/j.ipl.2015.05.012_br0080","series-title":"Proc. of the 35th ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages","first-page":"147","article-title":"Proving non-termination","author":"Gupta","year":"2008"},{"key":"10.1016\/j.ipl.2015.05.012_br0090","article-title":"MONA Version 1.4 User Manual","author":"Klarlund","year":"2001"},{"key":"10.1016\/j.ipl.2015.05.012_br0100","series-title":"Relational verification of programs with integer data","author":"Kone\u010dn\u00fd","year":"2012"},{"key":"10.1016\/j.ipl.2015.05.012_br0110","series-title":"Proc. of the 28th ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages","first-page":"81","article-title":"The size-change principle for program termination","author":"Lee","year":"2001"},{"key":"10.1016\/j.ipl.2015.05.012_br0120","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin","year":"1969","journal-title":"Trans. Am. Math. Soc."},{"issue":"3","key":"10.1016\/j.ipl.2015.05.012_br0130","doi-asserted-by":"crossref","DOI":"10.1145\/1709093.1709095","article-title":"A termination analyzer for Java bytecode based on path-length","volume":"32","author":"Spoto","year":"2010","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.ipl.2015.05.012_br0140","series-title":"Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics","first-page":"133","article-title":"Automata on infinite objects","author":"Thomas","year":"1990"},{"key":"10.1016\/j.ipl.2015.05.012_br0150","series-title":"Proc. of the 16th International Conference on Computer Aided Verification","first-page":"70","article-title":"Termination of linear programs","volume":"vol. 3114","author":"Tiwari","year":"2004"}],"container-title":["Information Processing Letters"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0020019015000897?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0020019015000897?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2021,10,26]],"date-time":"2021-10-26T03:40:23Z","timestamp":1635219623000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0020019015000897"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11]]},"references-count":15,"journal-issue":{"issue":"11","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["S0020019015000897"],"URL":"https:\/\/doi.org\/10.1016\/j.ipl.2015.05.012","relation":{},"ISSN":["0020-0190"],"issn-type":[{"value":"0020-0190","type":"print"}],"subject":[],"published":{"date-parts":[[2015,11]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"A second-order formulation of non-termination","name":"articletitle","label":"Article Title"},{"value":"Information Processing Letters","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.ipl.2015.05.012","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2015 Elsevier B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}