{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:49:15Z","timestamp":1775868555811,"version":"3.50.1"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"National Science Foundation","award":["CCF-1948536"],"award-info":[{"award-number":["CCF-1948536"]}]},{"DOI":"10.13039\/100000183","name":"Army Research Office","doi-asserted-by":"publisher","award":["W911NF-19-1-0054"],"award-info":[{"award-number":["W911NF-19-1-0054"]}],"id":[{"id":"10.13039\/100000183","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007297","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2787"],"award-info":[{"award-number":["N00014-17-1-2787"]}],"id":[{"id":"10.13039\/100007297","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>There is growing interest in termination reasoning for nonlinear programs and, meanwhile, recent dynamic strategies have shown they are able to infer invariants for such challenging programs. These advances led us to hypothesize that perhaps such dynamic strategies for nonlinear invariants could be adapted to learn recurrent sets (for non-termination) and\/or ranking functions (for termination).<\/jats:p>\n          <jats:p>In this paper, we exploit dynamic analysis and draw termination and non-termination as well as static and dynamic strategies closer together in order to tackle nonlinear programs. For termination, our algorithm infers ranking functions from concrete transitive closures, and, for non-termination, the algorithm iteratively collects executions and dynamically learns conditions to refine recurrent sets. Finally, we describe an integrated algorithm that allows these algorithms to mutually inform each other, taking counterexamples from a failed validation in one endeavor and crossing both the static\/dynamic and termination\/non-termination lines, to create new execution samples for the other one.<\/jats:p>\n          <jats:p>We have implemented these algorithms in a new tool called DynamiTe. For nonlinear programs, there are currently no SV-COMP termination benchmarks so we created new sets of 38 terminating and 39 non-terminating programs. Our empirical evaluation shows that we can effectively guess (and sometimes even validate) ranking functions and recurrent sets for programs with nonlinear behaviors. Furthermore, we show that counterexamples from one failed validation can be used to generate executions for a dynamic analysis of the opposite property. Although we are focused on nonlinear programs, as a point of comparison, we compare DynamiTe's performance on linear programs with that of the state-of-the-art tool, Ultimate. Although DynamiTe is an order of magnitude slower it is nonetheless somewhat competitive and sometimes finds ranking functions where Ultimate was unable to. Ultimate cannot, however, handle the nonlinear programs in our new benchmark suite.<\/jats:p>","DOI":"10.1145\/3428257","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:36:06Z","timestamp":1606260966000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["DynamiTe: dynamic termination and non-termination proofs"],"prefix":"10.1145","volume":"4","author":[{"given":"Ton Chanh","family":"Le","sequence":"first","affiliation":[{"name":"Stevens Institute of Technology, USA"}]},{"given":"Timos","family":"Antonopoulos","sequence":"additional","affiliation":[{"name":"Yale University, USA"}]},{"given":"Parisa","family":"Fathololumi","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, USA"}]},{"given":"Eric","family":"Koskinen","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, USA"}]},{"given":"ThanhVu","family":"Nguyen","sequence":"additional","affiliation":[{"name":"University of Nebraska-Lincoln, USA"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"AProVE. 2020. AProVE: Automated Program Verification Environment. http:\/\/aprove.informatik.rwth-aachen.de\/.  AProVE. 2020. AProVE: Automated Program Verification Environment. http:\/\/aprove.informatik.rwth-aachen.de\/."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2007.32"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_21"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_109"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_8"},{"key":"e_1_2_2_10_1","unstructured":"Marc Brockschmidt. 2020. T2: TEMPORAL LOGIC PROVER. https:\/\/github.com\/mmjb\/T2.  Marc Brockschmidt. 2020. T2: TEMPORAL LOGIC PROVER. https:\/\/github.com\/mmjb\/T2."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070545"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_11"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987597"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_32"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1941487.1941509"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103687"},{"key":"e_1_2_2_18_1","unstructured":"CPAChecker. 2020. CPAchecker: The Configurable Software-Verification Platform. https:\/\/cpachecker.sosy-lab.org\/.  CPAChecker. 2020. CPAchecker: The Configurable Software-Verification Platform. https:\/\/cpachecker.sosy-lab.org\/."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_4"},{"key":"e_1_2_2_21_1","unstructured":"DynamiTe. 2020. Supplemental Materials. https:\/\/github.com\/letonchanh\/dynamite.  DynamiTe. 2020. Supplemental Materials. https:\/\/github.com\/letonchanh\/dynamite."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Michael D Ernst Jef H Perkins Philip J Guo Stephen McCamant Carlos Pacheco Matthew S Tschantz and Chen Xiao. 2007. The Daikon system for dynamic detection of likely invariants. Science of computer programming 69 1-3 ( 2007 ) 35-45.  Michael D Ernst Jef H Perkins Philip J Guo Stephen McCamant Carlos Pacheco Matthew S Tschantz and Chen Xiao. 2007. The Daikon system for dynamic detection of likely invariants. Science of computer programming 69 1-3 ( 2007 ) 35-45.","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_4"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2019.8894271"},{"key":"e_1_2_2_26_1","unstructured":"FuncTion. 2020. FuncTion: An Abstract Domain Functor for Termination. https:\/\/www.di.ens.fr\/~urban\/FuncTion.html.  FuncTion. 2020. FuncTion: An Abstract Domain Functor for Termination. https:\/\/www.di.ens.fr\/~urban\/FuncTion.html."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_13"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25979-4_15"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_35"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_7"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani Krishna K Mehra and Trishul Chilimbi. 2009. Speed: precise and eficient static estimation of program computational complexity. ACM Sigplan Notices 44 1 ( 2009 ) 127-139.  Sumit Gulwani Krishna K Mehra and Trishul Chilimbi. 2009. Speed: precise and eficient static estimation of program computational complexity. ACM Sigplan Notices 44 1 ( 2009 ) 127-139.","DOI":"10.1145\/1594834.1480898"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328459"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_19"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926427"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2_13"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"e_1_2_2_39_1","volume-title":"DynamiTe: Dynamic Termination and Non-termination Proofs. arXiv","author":"Le Ton Chanh","year":"2010","unstructured":"Ton Chanh Le , Timos Antonopoulos , Parisa Fathololumi , Eric Koskinen , and ThanhVu Nguyen . 2020. DynamiTe: Dynamic Termination and Non-termination Proofs. arXiv : 2010 . 05747 [cs.PL] Ton Chanh Le, Timos Antonopoulos, Parisa Fathololumi, Eric Koskinen, and ThanhVu Nguyen. 2020. DynamiTe: Dynamic Termination and Non-termination Proofs. arXiv: 2010. 05747 [cs.PL]"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11737-9_18"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737993"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314634"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/647478.727796"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314643"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106281"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115691"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115691"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"e_1_2_2_50_1","volume-title":"DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants. ACM Transactions on Software Engineering and Methodology, to appear ( 2014 ).","author":"Nguyen ThanhVu","year":"2014","unstructured":"ThanhVu Nguyen , Deepak Kapur , Westley Weimer , and Stephanie Forrest . 2014 a. DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants. ACM Transactions on Software Engineering and Methodology, to appear ( 2014 ). ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. 2014a. DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants. ACM Transactions on Software Engineering and Methodology, to appear ( 2014 )."},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568275"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491413"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_2_2_54_1","doi-asserted-by":"crossref","unstructured":"Saswat Padhi Rahul Sharma and Todd Millstein. 2016. Data-driven precondition inference with learned features. ACM SIGPLAN Notices 51 6 ( 2016 ) 42-56.  Saswat Padhi Rahul Sharma and Todd Millstein. 2016. Data-driven precondition inference with learned features. ACM SIGPLAN Notices 51 6 ( 2016 ) 42-56.","DOI":"10.1145\/2980983.2908099"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319598"},{"key":"e_1_2_2_57_1","doi-asserted-by":"crossref","unstructured":"Enric Rodr\u00edguez-Carbonell and Deepak Kapur. 2007a. Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Science of Computer Programming 64 1 ( 2007 ) 54-75.  Enric Rodr\u00edguez-Carbonell and Deepak Kapur. 2007a. Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Science of Computer Programming 64 1 ( 2007 ) 54-75.","DOI":"10.1016\/j.scico.2006.03.003"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2807591.2807635"},{"key":"e_1_2_2_61_1","unstructured":"SV-COMP benchmark nla-digbench. 2020. SV-COMP benchmark nla-digbench. https:\/\/github.com\/sosy-lab\/svbenchmarks\/tree\/master\/c\/nla-digbench.  SV-COMP benchmark nla-digbench. 2020. SV-COMP benchmark nla-digbench. https:\/\/github.com\/sosy-lab\/svbenchmarks\/tree\/master\/c\/nla-digbench."},{"key":"e_1_2_2_62_1","unstructured":"Ultimate. 2020. Ultimate Automizer. https:\/\/monteverdi.informatik.uni-freiburg.de\/tomcat\/Website\/?ui=tool&tool=ltl_automizer.  Ultimate. 2020. Ultimate Automizer. https:\/\/monteverdi.informatik.uni-freiburg.de\/tomcat\/Website\/?ui=tool&tool=ltl_automizer."},{"key":"e_1_2_2_63_1","volume-title":"Piecewise-Defined Ranking Functions. In 13th International Workshop on Termination (WST 2013 ). 69","author":"Urban Caterina","year":"2013","unstructured":"Caterina Urban . 2013 . Piecewise-Defined Ranking Functions. In 13th International Workshop on Termination (WST 2013 ). 69 . Caterina Urban. 2013. Piecewise-Defined Ranking Functions. In 13th International Workshop on Termination (WST 2013 ). 69."},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_46"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_22"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133903"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385986"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428257","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428257","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428257","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428257"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":67,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428257"],"URL":"https:\/\/doi.org\/10.1145\/3428257","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}