{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:06Z","timestamp":1776333486661,"version":"3.51.2"},"reference-count":42,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.23919\/fmcad.2019.8894271","type":"proceedings-article","created":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T04:25:06Z","timestamp":1573619106000},"page":"221-230","source":"Crossref","is-referenced-by-count":18,"title":["Proving Non-Termination via Loop Acceleration"],"prefix":"10.23919","author":[{"given":"Florian","family":"Frohn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jurgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","year":"0","journal-title":"TPDB"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_52"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679413"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-015-0228-1"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_38"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542259"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_16"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737993"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2866575"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_4"},{"key":"ref11","first-page":"387","article-title":"T2: Temporal Property Verification","author":"brockschmidt","year":"2016","journal-title":"TACAS ’17"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192405"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_11"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987597"},{"key":"ref15","first-page":"337","article-title":"Z3: An Efficient SMT Solver","author":"de moura","year":"2008","journal-title":"TACAS ’08"},{"key":"ref16","first-page":"83","article-title":"iRankFinder","author":"domenech","year":"2018","journal-title":"WST ’18"},{"key":"ref17","first-page":"55","article-title":"Control-Flow Refinement via Partial Evaluation","author":"dom\u00e9nech","year":"2018","journal-title":"WST ’18"},{"key":"ref18","first-page":"737","article-title":"Yices 2.2","author":"dutertre","year":"2014","journal-title":"CAV ’14"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-0484-5"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_27"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328459"},{"key":"ref3","first-page":"133","article-title":"Automatic Verification of C and Java Programs: SV-COMP 2019","author":"beyer","year":"2019","journal-title":"TACAS ’95"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535843"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_6"},{"key":"ref8","author":"brockschmidt","year":"2014","journal-title":"TermComp Proposal Pushdown Systems as a Model for Programs with Procedures"},{"key":"ref7","first-page":"123","article-title":"Automated Detection of Non-termination and NullPointer-Exceptions for Java Bytecode","author":"brockschmidt","year":"2011","journal-title":"FoVeOOS ’11"},{"key":"ref2","article-title":"Multiphase-Linear Ranking Functions and their Relation to Recurrent Sets","author":"ben-amram","year":"2018","journal-title":"CoRR abs\/1811 07340"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542250"},{"key":"ref1","article-title":"PURRS: Towards Computer Algebra Support for Fully Automatic Worst-Case Complexity Analysis","author":"bagnara","year":"2005","journal-title":"CoRR abs\/cs\/0512056"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_16"},{"key":"ref22","article-title":"Proving Non-Termination via Loop Acceleration","author":"frohn","year":"2019","journal-title":"CoRR abs\/1905 111187"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_37"},{"key":"ref42","first-page":"519","article-title":"Mathematica: A System for Doing Mathematics by Computer","volume":"34 3","author":"wolfram","year":"1992","journal-title":"SIAM Review"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_10"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79124-9_11"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9388-y"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542518"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_10"}],"event":{"name":"2019 Formal Methods in Computer Aided Design (FMCAD)","location":"San Jose, CA, USA","start":{"date-parts":[[2019,10,22]]},"end":{"date-parts":[[2019,10,25]]}},"container-title":["2019 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8891869\/8894241\/08894271.pdf?arnumber=8894271","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,25]],"date-time":"2021-01-25T18:48:09Z","timestamp":1611600489000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8894271\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10]]},"references-count":42,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2019.8894271","relation":{},"subject":[],"published":{"date-parts":[[2019,10]]}}}