{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:00:44Z","timestamp":1762459244259,"version":"3.28.0"},"reference-count":34,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/fmcad.2014.6987597","type":"proceedings-article","created":{"date-parts":[[2014,12,31]],"date-time":"2014-12-31T01:00:39Z","timestamp":1419987639000},"page":"67-74","source":"Crossref","is-referenced-by-count":21,"title":["Disproving termination with overapproximation"],"prefix":"10.1109","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[]},{"given":"Carsten","family":"Fuhs","sequence":"additional","affiliation":[]},{"given":"Kaustubh","family":"Nimkar","sequence":"additional","affiliation":[]},{"given":"Peter","family":"O'Hearn","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","article-title":"Yasm: A software modelchecker for verification and refutation","volume":"6","author":"gurfinkel","year":"0","journal-title":"Proc CAV"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328459"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709095"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_13"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79124-9_11"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1007\/11559306_12"},{"key":"13","article-title":"Proving non-looping nontermination automatically","volume":"12","author":"emmes","year":"0","journal-title":"Proc IJCAR"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47813-2_9"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/s002000100065"},{"key":"21","article-title":"Solving non-linear arithmetic","volume":"12","author":"jovanovic","year":"0","journal-title":"Proc IJCAR"},{"key":"20","article-title":"Apron: A library of numerical abstract domains for static analysis","volume":"9","author":"jeannet","year":"0","journal-title":"Proc CAV"},{"key":"22","article-title":"Termination analysis with compositional transition invariants","volume":"10","author":"kroening","year":"0","journal-title":"Proc CAV"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_52"},{"journal-title":"Instrumentation Analysis An Automated Method for Producing Numeric Abstractions of Heap-Manipulating Programs","year":"2010","author":"magill","key":"24"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706326"},{"key":"26","first-page":"1","article-title":"The octagon abstract domain","volume":"19","author":"min\ufffd","year":"2006","journal-title":"Higher-Order and Symbolic Computation"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1145\/69558.69559"},{"key":"28","article-title":"Local reasoning about programs that alter data structures","volume":"1","author":"o'hearn","year":"0","journal-title":"Proceedings CSL"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.05.013"},{"key":"3","article-title":"Automatic termination proofs for programs with shape-shifting heaps","volume":"6","author":"berdine","year":"0","journal-title":"Proc CAV"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_19"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491969"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.11.002"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068409003652"},{"key":"7","article-title":"Automated detection of non-termination and nullpointer-exceptions for java bytecode","volume":"11","author":"brockschmidt","year":"0","journal-title":"Proc FoVeOOS"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_28"},{"key":"32","article-title":"Pushdown model checking for malware detection","volume":"12","author":"song","year":"0","journal-title":"Proc TACAS"},{"key":"5","article-title":"Linear ranking with reachability","author":"bradley","year":"0","journal-title":"Proceedings of CAV'05"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.11.016"},{"key":"4","article-title":"Programs with lists are counter automata","volume":"6","author":"bouajjani","year":"0","journal-title":"Proc CAV"},{"key":"9","article-title":"Linear invariant generation using non-linear constraint solving","volume":"3","author":"col\ufffdn","year":"0","journal-title":"Proc CAV"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_11"}],"event":{"name":"2014 Formal Methods in Computer-Aided Design (FMCAD)","start":{"date-parts":[[2014,10,21]]},"location":"Lausanne, Switzerland","end":{"date-parts":[[2014,10,24]]}},"container-title":["2014 Formal Methods in Computer-Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6975680\/6987576\/06987597.pdf?arnumber=6987597","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,24]],"date-time":"2017-03-24T00:51:21Z","timestamp":1490316681000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6987597\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":34,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2014.6987597","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}