{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:46:58Z","timestamp":1775868418850,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,8,21]],"date-time":"2017-08-21T00:00:00Z","timestamp":1503273600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61572349, 61272106"],"award-info":[{"award-number":["61572349, 61272106"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001381","name":"National Research Foundation Singapore","doi-asserted-by":"publisher","award":["NRF2014NCR-NCR001-30"],"award-info":[{"award-number":["NRF2014NCR-NCR001-30"]}],"id":[{"id":"10.13039\/501100001381","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,8,21]]},"DOI":"10.1145\/3106237.3106260","type":"proceedings-article","created":{"date-parts":[[2017,8,2]],"date-time":"2017-08-02T19:36:18Z","timestamp":1501702578000},"page":"84-94","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Loopster: static loop termination analysis"],"prefix":"10.1145","author":[{"given":"Xiaofei","family":"Xie","sequence":"first","affiliation":[{"name":"Tianjin University, China"}]},{"given":"Bihuan","family":"Chen","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}]},{"given":"Liang","family":"Zou","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}]},{"given":"Shang-Wei","family":"Lin","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}]},{"given":"Xiaohong","family":"Li","sequence":"additional","affiliation":[{"name":"Tianjin University, China"}]}],"member":"320","published-online":{"date-parts":[[2017,8,21]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Competition on Software Verification","year":"2016","unstructured":"2016. Competition on Software Verification 2016 . http:\/\/sv-comp.sosy-lab.org\/ 2016. (2016). 2017. 2LS for Program Analysis . http:\/\/www.cprover.org\/wiki\/doku.php?id=2ls_ for_program_analysis. (2017). 2017. llvm2kittel. (2017). https:\/\/github.com\/s-falke\/llvm2kittel. 2017. LLVM\u2019s Analysis and Transform Passes. http:\/\/llvm.org\/docs\/Passes.html. (2017). 2017. Loopster. https:\/\/sites.google.com\/site\/looptermination. (2017). 2016. Competition on Software Verification 2016. http:\/\/sv-comp.sosy-lab.org\/ 2016. (2016). 2017. 2LS for Program Analysis. http:\/\/www.cprover.org\/wiki\/doku.php?id=2ls_ for_program_analysis. (2017). 2017. llvm2kittel. (2017). https:\/\/github.com\/s-falke\/llvm2kittel. 2017. LLVM\u2019s Analysis and Transform Passes. http:\/\/llvm.org\/docs\/Passes.html. (2017). 2017. Loopster. https:\/\/sites.google.com\/site\/looptermination. (2017)."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_19"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629488"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_35"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_109"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_37"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Marc Brockschmidt Byron Cook and Carsten Fuhs. 2013. Better termination proving through cooperation. In CAV. 413\u2013429.  Marc Brockschmidt Byron Cook and Carsten Fuhs. 2013. Better termination proving through cooperation. In CAV. 413\u2013429.","DOI":"10.1007\/978-3-642-39799-8_28"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Hong-Yi Chen Byron Cook Carsten Fuhs Kaustubh Nimkar and Peter O\u2019Hearn. 2014. Proving nontermination via safety. In TACAS. 156\u2013171.  Hong-Yi Chen Byron Cook Carsten Fuhs Kaustubh Nimkar and Peter O\u2019Hearn. 2014. Proving nontermination via safety. In TACAS. 156\u2013171.","DOI":"10.1007\/978-3-642-54862-8_11"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Hong-Yi Chen Daniel Kroening Peter Schrammel and Bjoern Wachter. 2015. Synthesising Interprocedural Bit-Precise Termination Proofs. In ASE. 53\u201364.  Hong-Yi Chen Daniel Kroening Peter Schrammel and Bjoern Wachter. 2015. Synthesising Interprocedural Bit-Precise Termination Proofs. In ASE. 53\u201364.","DOI":"10.1109\/ASE.2015.10"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Alias Christophe Darte Alain Feautrier Paul and Gonnord Laure. 2010. Multidimensional Rankings Program Termination and Complexity Bounds of Flowchart Programs. In SAS. 117\u2013133.   Alias Christophe Darte Alain Feautrier Paul and Gonnord Laure. 2010. Multidimensional Rankings Program Termination and Complexity Bounds of Flowchart Programs. In SAS. 117\u2013133.","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"e_1_3_2_1_12_1","volume-title":"SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers. CoRR","author":"Codish Michael","year":"2011","unstructured":"Michael Codish , Igor Gonopolskiy , Amir M. Ben-Amram , Carsten Fuhs , and J\u00fcrgen Giesl . 2011. SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers. CoRR ( 2011 ). Michael Codish, Igor Gonopolskiy, Amir M. Ben-Amram, Carsten Fuhs, and J\u00fcrgen Giesl. 2011. SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers. CoRR (2011)."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190257"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Byron Cook Eric Koskinen and Moshe Vardi. 2011. Temporal property verification as a program analysis task. In CAV. 333\u2013348.   Byron Cook Eric Koskinen and Moshe Vardi. 2011. Temporal property verification as a program analysis task. In CAV. 333\u2013348.","DOI":"10.1007\/978-3-642-22110-1_26"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_19"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1941487.1941509"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Cristina David Daniel Kroening and Matt Lewis. 2015. Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs. In ESOP. 183\u2013204.  Cristina David Daniel Kroening and Matt Lewis. 2015. Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs. In ESOP. 183\u2013204.","DOI":"10.1007\/978-3-662-46669-8_8"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS. 337\u2013340.   Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS. 337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806630"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328459"},{"key":"e_1_3_2_1_24_1","volume-title":"Rajamani","author":"Harris William R.","year":"2010","unstructured":"William R. Harris , Akash Lal , Aditya V. Nori , and Sriram K . Rajamani . 2010 . Alternation for Termination. In SAS. 304\u2013319. William R. Harris, Akash Lal, Aditya V. Nori, and Sriram K. Rajamani. 2010. Alternation for Termination. In SAS. 304\u2013319."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_68"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_9"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_52"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Daniel Larraz Albert Oliveras Enric Rodr\u00edguez-Carbonell and Albert Rubio. 2013. Proving termination of imperative programs using Max-SMT. In FMCAD. 218\u2013225.  Daniel Larraz Albert Oliveras Enric Rodr\u00edguez-Carbonell and Albert Rubio. 2013. Proving termination of imperative programs using Max-SMT. In FMCAD. 218\u2013225.","DOI":"10.1109\/FMCAD.2013.6679413"},{"key":"e_1_3_2_1_31_1","volume-title":"LLVM: A compilation framework for lifelong program analysis &amp","author":"Lattner Chris","year":"2004","unstructured":"Chris Lattner and Vikram Adve . 2004 . LLVM: A compilation framework for lifelong program analysis &amp ; transformation. In CGO. 75\u201388. Chris Lattner and Vikram Adve. 2004. LLVM: A compilation framework for lifelong program analysis & transformation. In CGO. 75\u201388."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Jan Leike and Matthias Heizmann. 2014. Ranking Templates for Linear Loops. In TACAS. 172\u2013186.  Jan Leike and Matthias Heizmann. 2014. Ranking Templates for Linear Loops. In TACAS. 172\u2013186.","DOI":"10.1007\/978-3-642-54862-8_12"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2009.17"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.391376"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Col\u00f3n Michael and Sipma Henny. 2001. Synthesis of Linear Ranking Functions. In TACAS. 67\u201381.  Col\u00f3n Michael and Sipma Henny. 2001. Synthesis of Linear Ranking Functions. In TACAS. 67\u201381.","DOI":"10.1007\/3-540-45319-9_6"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Col\u00f3n Michael and Sipma Henny. 2002. Practical Methods for Proving Program Termination. In CAV. 442\u2013454.   Col\u00f3n Michael and Sipma Henny. 2002. Practical Methods for Proving Program Termination. In CAV. 442\u2013454.","DOI":"10.1007\/3-540-45657-0_36"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/800020.808263"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Andreas Podelski and Andrey Rybalchenko. 2004. A complete method for the synthesis of linear ranking functions. In VMCAI. 239\u2013251.  Andreas Podelski and Andrey Rybalchenko. 2004. A complete method for the synthesis of linear ranking functions. In VMCAI. 239\u2013251.","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69611-7_16"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_7"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Helga Velroyen and Philipp R\u00fcmmer. 2008. Non-termination Checking for Imperative Programs. In TAP. 154\u2013170.   Helga Velroyen and Philipp R\u00fcmmer. 2008. Non-termination Checking for Imperative Programs. In TAP. 154\u2013170.","DOI":"10.1007\/978-3-540-79124-9_11"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950340"}],"event":{"name":"ESEC\/FSE'17: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering","location":"Paderborn Germany","acronym":"ESEC\/FSE'17","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3106237.3106260","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3106237.3106260","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:37Z","timestamp":1750217437000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3106237.3106260"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,21]]},"references-count":41,"alternative-id":["10.1145\/3106237.3106260","10.1145\/3106237"],"URL":"https:\/\/doi.org\/10.1145\/3106237.3106260","relation":{},"subject":[],"published":{"date-parts":[[2017,8,21]]},"assertion":[{"value":"2017-08-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}