{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:35:52Z","timestamp":1774838152061,"version":"3.50.1"},"publisher-location":"New York, New York, USA","reference-count":55,"publisher":"ACM Press","license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100008982","name":"National Science Foundation","doi-asserted-by":"publisher","award":["#1763922.,#1846350"],"award-info":[{"award-number":["#1763922.,#1846350"]}],"id":[{"id":"10.13039\/501100008982","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1145\/3314221.3314643","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"845-859","source":"Crossref","is-referenced-by-count":8,"title":["Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs"],"prefix":"10.1145","author":[{"given":"Ph\u00fac C.","family":"Nguy\u1ec5n","sequence":"first","affiliation":[{"name":"University of Maryland at College Park, USA"}]},{"given":"Thomas","family":"Gilray","sequence":"additional","affiliation":[{"name":"University of Alabama at Birmingham, USA"}]},{"given":"Sam","family":"Tobin-Hochstadt","sequence":"additional","affiliation":[{"name":"Indiana University, USA"}]},{"given":"David","family":"Van Horn","sequence":"additional","affiliation":[{"name":"University of Maryland at College Park, USA"}]}],"member":"320","reference":[{"key":"key-10.1145\/3314221.3314643-1","unstructured":"Elvira Albert, Puri Arenas, Michael Codish, Samir Genaim, Germán Puebla, and Damiano Zanardini. 2008. Termination analysis of Java bytecode. In International Conference on Formal Methods for Open Object-Based Distributed Systems. Springer, 2–18."},{"key":"key-10.1145\/3314221.3314643-2","unstructured":"Thomas Arts and Jürgen Giesl. 2000. Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 1-2 (2000), 133–178."},{"key":"#cr-split#-key-10.1145\/3314221.3314643-3.1","doi-asserted-by":"crossref","unstructured":"James Bailey, Alexandra Poulovassilis, and Peter Newson. 2000. A Dynamic Approach to Termination Analysis for Active Database Rules. In Computational Logic &#8212","DOI":"10.1007\/3-540-44957-4_74"},{"key":"#cr-split#-key-10.1145\/3314221.3314643-3.2","unstructured":"CL 2000, John Lloyd, Veronica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luís Moniz Pereira, Yehoshua Sagiv, and Peter J. Stuckey (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1106–1120."},{"key":"key-10.1145\/3314221.3314643-4","unstructured":"Josh Berdine, Byron Cook, Dino Distefano, and Peter W O’hearn. 2006. Automatic termination proofs for programs with shape-shifting heaps. In International Conference on Computer Aided Verification. Springer, 386–400."},{"key":"key-10.1145\/3314221.3314643-5","unstructured":"Marc Brockschmidt, Richard Musiol, Carsten Otto, and Jürgen Giesl. 2012. Automated termination proofs for Java programs with cyclic data. In International Conference on Computer Aided Verification. Springer, 105–122."},{"key":"key-10.1145\/3314221.3314643-6","unstructured":"Jacob Burnim, Nicholas Jalbert, Christos Stergiou, and Koushik Sen. 2009. Looper: Lightweight detection of infinite loops at runtime. In Proceedings of the 2009 IEEE\/ACM International Conference on Automated Software Engineering. IEEE Computer Society, 161–169."},{"key":"key-10.1145\/3314221.3314643-7","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. USENIX Association."},{"key":"key-10.1145\/3314221.3314643-8","unstructured":"Michael Carbin, Sasa Misailovic, Michael Kling, and Martin C Rinard. 2011. Detecting and escaping infinite loops with Jolt. In European Conference on Object-Oriented Programming. Springer, 609–633."},{"key":"key-10.1145\/3314221.3314643-9","unstructured":"Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2003. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM (JACM) 50, 5 (2003), 752– 794."},{"key":"key-10.1145\/3314221.3314643-10","doi-asserted-by":"crossref","unstructured":"John Clements and Matthias Felleisen. 2004. A Tail-recursive Machine with Stack Inspection. ACM Trans. Program. Lang. Syst. 26, 6 (Nov. 2004).","DOI":"10.1145\/1034774.1034778"},{"key":"key-10.1145\/3314221.3314643-11","unstructured":"Michael Codish, Vitaly Lagoon, and Peter J. Stuckey. 2005. Testing for Termination with Monotonicity Constraints. In Logic Programming, Maurizio Gabbrielli and Gopal Gupta (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 326–340."},{"key":"key-10.1145\/3314221.3314643-12","unstructured":"Michael Codish and Cohavit Taboch. 1997. A Semantic Basis for Termination Analysis of Logic Programs and Its Realization Using Symbolic Norm Constraints. In Proceedings of the 6th International Joint Conference on Algebraic and Logic Programming (ALP ’97-HOA ’97). Springer-Verlag, London, UK, UK, 31–45."},{"key":"key-10.1145\/3314221.3314643-13","unstructured":"Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Termination proofs for systems code. In Proceedings of the 27th ACM SIG-PLAN Conference on Programming Language Design and Implementation, Vol. 41. ACM, 415–426."},{"key":"key-10.1145\/3314221.3314643-14","unstructured":"Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. TER-MINATOR: beyond safety. In International Conference on Computer Aided Verification. Springer, 415–418."},{"key":"key-10.1145\/3314221.3314643-15","doi-asserted-by":"crossref","unstructured":"David Darais, Nicholas Labich, Phúc C. Nguyễn, and David Van Horn. 2017. Abstracting Definitional Interpreters (Functional Pearl). Proc. ACM Program. Lang. 1, ICFP, Article 12 (Aug. 2017), 25 pages.","DOI":"10.1145\/3110256"},{"key":"key-10.1145\/3314221.3314643-16","unstructured":"Martin Davis. 1958. Computability and Unsolvability. McGraw-Hill."},{"key":"key-10.1145\/3314221.3314643-17","doi-asserted-by":"crossref","unstructured":"Robert B. Findler and Matthias Felleisen. 2002. Contracts for higherorder functions. In ICFP ’02: Proceedings of the seventh ACM SIGPLAN International Conference on Functional Programming. ACM.","DOI":"10.1145\/581478.581484"},{"key":"key-10.1145\/3314221.3314643-18","unstructured":"Jürgen Giesl, Matthias Raffelsieper, Peter Schneider-Kamp, Stephan Swiderski, and René Thiemann. 2011. Automated termination proofs for Haskell by term rewriting. ACM Transactions on Programming Languages and Systems (TOPLAS) 33, 2 (2011), 7."},{"key":"key-10.1145\/3314221.3314643-19","unstructured":"Jürgen Giesl, Peter Schneider-Kamp, and René Thiemann. 2006. AProVE 1.2: Automatic termination proofs in the dependency pair framework. In International Joint Conference on Automated Reasoning. Springer, 281–286."},{"key":"key-10.1145\/3314221.3314643-20","unstructured":"Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp. 2005. The dependency pair framework: Combining techniques for automated termination proofs. In International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer, 301–331."},{"key":"key-10.1145\/3314221.3314643-21","unstructured":"Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp. 2005. Proving and Disproving Termination of Higher-Order Functions. In Frontiers of Combining Systems, Bernhard Gramlich (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 216–231."},{"key":"key-10.1145\/3314221.3314643-22","unstructured":"Jürgen Giesl, René Thiemann, Stephan Swiderski, and Peter Schneider-Kamp. 2007. Proving termination by bounded increase. In International Conference on Automated Deduction. Springer, 443–459."},{"key":"key-10.1145\/3314221.3314643-23","unstructured":"Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, and Ru-Gang Xu. 2008. Proving Non-termination. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL ’08). ACM, 147–158."},{"key":"key-10.1145\/3314221.3314643-24","unstructured":"Matthias Heizmann, Neil D Jones, and Andreas Podelski. 2010. Sizechange termination and transition invariants. In International Static Analysis Symposium. Springer, 22–50."},{"key":"key-10.1145\/3314221.3314643-25","unstructured":"Neil D Jones and Nina Bohr. 2004. Termination analysis of the untyped 𝜆-calculus. In International Conference on Rewriting Techniques and Applications. Springer, 1–23."},{"key":"key-10.1145\/3314221.3314643-26","doi-asserted-by":"crossref","unstructured":"James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM 19, 7 (1976).","DOI":"10.1145\/360248.360252"},{"key":"key-10.1145\/3314221.3314643-27","unstructured":"Michael Kling, Sasa Misailovic, Michael Carbin, and Martin Rinard. 2012. Bolt: on-demand infinite loop escape in unmodified binaries. In Proceedings of the ACM international conference on Object oriented programming systems languages and applications, Vol. 47. ACM, 431– 450."},{"key":"key-10.1145\/3314221.3314643-28","unstructured":"Alexander Krauss. 2007. Certified size-change termination. In International Conference on Automated Deduction. Springer, 460–475."},{"key":"key-10.1145\/3314221.3314643-29","unstructured":"Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. 2001. The Size-change Principle for Program Termination. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’01). ACM, New York, NY, USA, 81–92."},{"key":"key-10.1145\/3314221.3314643-30","doi-asserted-by":"crossref","unstructured":"R. Majumdar and K. Sen. 2007. Hybrid Concolic Testing, In Software Engineering, 2007. ICSE 2007. 29th International Conference on. Software Engineering, 2007. ICSE 2007. 29th International Conference on (2007).","DOI":"10.1109\/ICSE.2007.41"},{"key":"key-10.1145\/3314221.3314643-31","unstructured":"Panagiotis Manolios and Daron Vroon. 2006. Termination analysis with calling context graphs. In International Conference on Computer Aided Verification. Springer, 401–414."},{"key":"key-10.1145\/3314221.3314643-32","doi-asserted-by":"crossref","unstructured":"Jan Midtgaard. 2012. Control-flow Analysis of Functional Programs. ACM Comput. Surv. 44, 3 (June 2012).","DOI":"10.1145\/2187671.2187672"},{"key":"key-10.1145\/3314221.3314643-33","unstructured":"Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn. 2018. Soft contract verification for higher-order stateful programs. PACMPL 2, POPL (2018), 51:1–51:30."},{"key":"key-10.1145\/3314221.3314643-34","unstructured":"Phúc C Nguyễn, Sam Tobin-Hochstadt, and David Van Horn. 2014. Soft Contract Verification. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. ACM."},{"key":"key-10.1145\/3314221.3314643-35","unstructured":"Sven Eric Panitz and Manfred Schmidt-Schauß. 1997. TEA: Automatically proving termination of programs in a non-strict higher-order functional language. In Static Analysis, Pascal Van Hentenryck (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 345–360."},{"key":"key-10.1145\/3314221.3314643-36","unstructured":"Andreas Podelski and Andrey Rybalchenko. 2004. A complete method for the synthesis of linear ranking functions. In International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 239–251."},{"key":"key-10.1145\/3314221.3314643-37","unstructured":"Andreas Podelski and Andrey Rybalchenko. 2004. Transition invariants. In Logic in Computer Science, 2004. Proceedings of the 19th Annual IEEE Symposium on. IEEE, 32–41."},{"key":"key-10.1145\/3314221.3314643-38","unstructured":"Koushik Sen. 2007. Concolic testing. In Proceedings of the twentysecond IEEE\/ACM international conference on Automated software engineering. ACM."},{"key":"key-10.1145\/3314221.3314643-39","doi-asserted-by":"crossref","unstructured":"Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: a concolic unit testing engine for C. SIGSOFT Softw. Eng. Notes 30, 5 (2005).","DOI":"10.1145\/1095430.1081750"},{"key":"key-10.1145\/3314221.3314643-40","doi-asserted-by":"crossref","unstructured":"Damien Sereni. 2006. Termination analysis of higher-order functional programs. Ph.D. Dissertation. Oxford University.","DOI":"10.1007\/11575467_19"},{"key":"key-10.1145\/3314221.3314643-41","unstructured":"Damien Sereni and Neil D. Jones. 2005. Termination Analysis of Higher-Order Functional Programs. In Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings, Vol. 3780. Springer."},{"key":"key-10.1145\/3314221.3314643-42","unstructured":"Yi-Dong Shen, Jia-Huai You, Li-Yan Yuan, Samuel S. P. Shen, and Qiang Yang. 2003. A Dynamic Approach to Characterizing Termination of General Logic Programs. ACM Trans. Comput. Logic 4, 4 (Oct. 2003), 417–430."},{"key":"key-10.1145\/3314221.3314643-43","unstructured":"Jeffrey Mark Siskind and Barak A. Pearlmutter. 2007. First-class Nonstandard Interpretations by Opening Closures. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’07). ACM, New York, NY, USA, 71–76."},{"key":"key-10.1145\/3314221.3314643-44","unstructured":"Fausto Spoto, Fred Mesnard, and Étienne Payet. 2010. A termination analyzer for Java bytecode based on path-length. ACM Transactions on Programming Languages and Systems (TOPLAS) 32, 3 (2010), 8."},{"key":"key-10.1145\/3314221.3314643-45","unstructured":"René Thiemann and Jürgen Giesl. 2003. Size-change termination for term rewriting. In International Conference on Rewriting Techniques and Applications. Springer, 264–278."},{"key":"key-10.1145\/3314221.3314643-46","doi-asserted-by":"crossref","unstructured":"Sam Tobin-Hochstadt and David Van Horn. 2012. Higher-order symbolic execution via contracts. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications. ACM.","DOI":"10.1145\/2384616.2384655"},{"key":"key-10.1145\/3314221.3314643-47","unstructured":"Aliaksei Tsitovich, Natasha Sharygina, Christoph M Wintersteiger, and Daniel Kroening. 2011. Loop summarization and termination analysis. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 81–95."},{"key":"key-10.1145\/3314221.3314643-48","unstructured":"Alan M. Turing. 1937. On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society s2-42, 1 (1937), 230–265."},{"key":"key-10.1145\/3314221.3314643-49","doi-asserted-by":"crossref","unstructured":"David Van Horn and Matthew Might. 2010. Abstracting Abstract Machines. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming. ACM.","DOI":"10.1145\/1863543.1863553"},{"key":"key-10.1145\/3314221.3314643-50","doi-asserted-by":"crossref","unstructured":"David Van Horn and Matthew Might. 2011. Abstracting abstract machines: a systematic approach to higher-order program analysis. Commun. ACM 54 (Sept. 2011).","DOI":"10.1145\/1995376.1995400"},{"key":"key-10.1145\/3314221.3314643-51","unstructured":"Niki Vazou, Eric L Seidel, and Ranjit Jhala. 2014. From Safety To Termination And Back: SMT-Based Verification For Lazy Languages. arXiv preprint arXiv:1401.6227 (2014)."},{"key":"key-10.1145\/3314221.3314643-52","doi-asserted-by":"crossref","unstructured":"Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon P. Jones. 2014. Refinement Types for Haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. ACM.","DOI":"10.1145\/2628136.2628161"},{"key":"key-10.1145\/3314221.3314643-53","unstructured":"Helga Velroyen and Philipp Rümmer. 2008. Non-termination checking for imperative programs. In International Conference on Tests and Proofs. Springer, 154–170."},{"key":"key-10.1145\/3314221.3314643-54","unstructured":"Hongwei Xi. 2002. Dependent types for program termination verification. Higher-Order and Symbolic Computation 15, 1 (2002), 91–131."}],"event":{"name":"the 40th ACM SIGPLAN Conference","location":"Phoenix, AZ, USA","acronym":"PLDI 2019","number":"40","sponsor":["SIGPLAN, ACM Special Interest Group on Programming Languages"],"start":{"date-parts":[[2019,6,22]]},"end":{"date-parts":[[2019,6,26]]}},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI 2019"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314643","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/dl.acm.org\/ft_gateway.cfm?id=3314643&ftid=2065495&dwn=1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:29Z","timestamp":1750204409000},"score":1,"resource":{"primary":{"URL":"http:\/\/dl.acm.org\/citation.cfm?doid=3314221.3314643"}},"subtitle":[],"proceedings-subject":"Programming Language Design and Implementation","short-title":[],"issued":{"date-parts":[[2019]]},"references-count":55,"URL":"https:\/\/doi.org\/10.1145\/3314221.3314643","relation":{},"subject":[],"published":{"date-parts":[[2019]]}}}