{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T04:13:37Z","timestamp":1746072817464,"version":"3.40.4"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906428","type":"print"},{"value":"9783031906435","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The Infinite Descent property underpins key verification techniques, such as size-change program termination and cyclic proofs. Deciding whether the Infinite Descent property holds of a given program or cyclic deduction is PSPACE-complete, with several exponential time algorithms in the literature. In this paper, we consider algorithms with better time complexity but which are (necessarily) <jats:italic>incomplete<\/jats:italic>. Concretely, we formulate and evaluate a number of alternative algorithms for semi-deciding Infinite Descent. Our aim is to improve average runtime performance by utilising more efficient algorithms for specific subclasses of input. We present <jats:sc>Cyclone<\/jats:sc>, a tool integrating these algorithms with an existing (complete) decision procedure. We evaluate <jats:sc>Cyclone<\/jats:sc> on a large suite of examples harvested from the  theorem prover, finding that the incomplete algorithms achieve extremely high coverage and afford substantial runtime improvement in practice. We thus believe that the <jats:sc>Cyclone<\/jats:sc> tool will foster broader adoption of techniques based on Infinite Descent and expand their practical applications.<\/jats:p>","DOI":"10.1007\/978-3-031-90643-5_18","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:08:05Z","timestamp":1745993285000},"page":"336-354","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Cyclone: A Heterogeneous Tool for Verifying Infinite Descent"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6608-3000","authenticated-orcid":false,"given":"Liron","family":"Cohen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4271-9078","authenticated-orcid":false,"given":"Reuben N. S.","family":"Rowe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-1150-0367","authenticated-orcid":false,"given":"Matan","family":"Shaked","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"18_CR1","unstructured":"Agda Developers: Agda, https:\/\/agda.readthedocs.io\/"},{"key":"18_CR2","unstructured":"Brotherston, J.: Sequent Calculus Proof Systems for Inductive Definitions. Ph.D. thesis, University of Edinburgh (November 2006), https:\/\/era.ed.ac.uk\/handle\/1842\/1458"},{"key":"18_CR3","doi-asserted-by":"publisher","unstructured":"Brotherston, J., Bornat, R., Calcagno, C.: Cyclic Proofs of Program Termination in Separation Logic. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008. pp. 101\u2013112. ACM (2008). https:\/\/doi.org\/10.1145\/1328438.1328453","DOI":"10.1145\/1328438.1328453"},{"key":"18_CR4","doi-asserted-by":"publisher","unstructured":"Brotherston, J., Gorogiannis, N.: Cyclic Abduction of Inductively Defined Safety and Termination Preconditions. In: M\u00fcller-Olm, M., Seidl, H. (eds.) Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08723, pp. 68\u201384. Springer (2014).https:\/\/doi.org\/10.1007\/978-3-319-10936-7_5","DOI":"10.1007\/978-3-319-10936-7_5"},{"key":"18_CR5","doi-asserted-by":"publisher","unstructured":"Brotherston, J., Gorogiannis, N., Petersen, R.L.: A Generic Cyclic Theorem Prover. In: Jhala, R., Igarashi, A. (eds.) Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings. Lecture Notes in Computer Science, vol.\u00a07705, pp. 350\u2013367. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-35182-2_25","DOI":"10.1007\/978-3-642-35182-2_25"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Brotherston, J., Simpson, A.: Sequent Calculi for Induction and Infinite Descent. Journal of Logic and Computation 21(6), 1177\u20131216 (2010). https:\/\/doi.org\/10.1093\/logcom\/exq052","DOI":"10.1093\/logcom\/exq052"},{"key":"18_CR7","unstructured":"Cheng, K.S., Ngan, C.W., Trung, T.Q., Chanh, L.T., Sivaraman, A., Toan, N.T.: Songbird Prover (2016), https:\/\/songbird-prover.github.io\/"},{"key":"18_CR8","doi-asserted-by":"publisher","unstructured":"Cohen, L., Jabarin, A., Popescu, A., Rowe, R.N.S.: The Complex(ity) Landscape of Checking Infinite Descent. Proceedings of the ACM on Programming Languages 8(POPL), 1352-1384 (Jan 2024). https:\/\/doi.org\/10.1145\/3632888","DOI":"10.1145\/3632888"},{"key":"18_CR9","doi-asserted-by":"publisher","unstructured":"Cohen, L., Rowe, R.N.S.: Non-Well-Founded Proof Theory of Transitive Closure Logic. ACM Trans. Comput. Logic 21(4) (Aug 2020). https:\/\/doi.org\/10.1145\/3404889","DOI":"10.1145\/3404889"},{"key":"18_CR10","doi-asserted-by":"publisher","unstructured":"Das, A.: On The Logical Complexity of Cyclic Arithmetic. Log. Methods Comput. Sci. 16(1) (2020). https:\/\/doi.org\/10.23638\/LMCS-16(1:1)2020","DOI":"10.23638\/LMCS-16(1:1)2020"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Dax, C., Hofmann, M., Lange, M.: A Proof System for the Linear Time $$\\rm \\mu $$-Calculus. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings. Lecture Notes in Computer Science, vol.\u00a04337, pp. 273\u2013284. Springer (2006). https:\/\/doi.org\/10.1007\/11944836_26","DOI":"10.1007\/11944836_26"},{"key":"18_CR12","doi-asserted-by":"publisher","unstructured":"Doumane, A.: Constructive Completeness for the Linear-time $$\\mu $$-calculus. In: Proceedings of the 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017. pp. 1\u201312 (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005075","DOI":"10.1109\/LICS.2017.8005075"},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Itzhaky, S., Peleg, H., Polikarpova, N., Rowe, R.N.S., Sergey, I.: Cyclic Program Synthesis. In: Freund, S.N., Yahav, E. (eds.) PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021. pp. 944\u2013959. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454087","DOI":"10.1145\/3453483.3454087"},{"key":"18_CR14","doi-asserted-by":"publisher","unstructured":"Jones, E., Ong, C.H.L., Ramsay, S.: CycleQ: An Efficient Basis for Cyclic Equational Reasoning. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. pp. 395\u2013409. PLDI 2022, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3519939.3523731","DOI":"10.1145\/3519939.3523731"},{"key":"18_CR15","doi-asserted-by":"publisher","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The Size-Change Principle for Program Termination. In: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. POPL01, ACM (Jan 2001). https:\/\/doi.org\/10.1145\/360204.360210","DOI":"10.1145\/360204.360210"},{"key":"18_CR16","doi-asserted-by":"publisher","unstructured":"Lehmann, D.J.: Algebraic Structures for Transitive Closure. Theor. Comput. Sci. 4(1), 59\u201376 (1977). https:\/\/doi.org\/10.1016\/0304-3975(77)90056-1","DOI":"10.1016\/0304-3975(77)90056-1"},{"key":"18_CR17","doi-asserted-by":"publisher","unstructured":"Lepigre, R., Raffalli, C.: Practical Subtyping for Curry-Style Languages. ACM Trans. Program. Lang. Syst. 41(1), 5:1\u20135:58 (2019). https:\/\/doi.org\/10.1145\/3285955","DOI":"10.1145\/3285955"},{"key":"18_CR18","doi-asserted-by":"publisher","unstructured":"Nollet, R., Saurin, A., Tasson, C.: PSPACE-Completeness of a Thread Criterion for Circular Proofs in Linear Logic with Least and Greatest fixed points. In: Cerrito, S., Popescu, A. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11714, pp. 317\u2013334. Springer (2019).https:\/\/doi.org\/10.1007\/978-3-030-29026-9_18","DOI":"10.1007\/978-3-030-29026-9_18"},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"Rowe, R., Cohen, L., Shaked, M.: Cyclone: A Heterogeneous Tool for Checking Infinite Descent (Software Artifact) (2025). https:\/\/doi.org\/10.5281\/zenodo.14743891","DOI":"10.5281\/zenodo.14743891"},{"key":"18_CR20","doi-asserted-by":"publisher","unstructured":"Rowe, R.N.S., Brotherston, J.: Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic. In: Bertot, Y., Vafeiadis, V. (eds.) Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. pp. 53\u201365. ACM (2017). https:\/\/doi.org\/10.1145\/3018610.3018623","DOI":"10.1145\/3018610.3018623"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Santocanale, L.: A Calculus of Circular Proofs and Its Categorical Semantics. In: Nielsen, M., Engberg, U. (eds.) Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2002. pp. 357\u2013371. Berlin, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45931-6_25","DOI":"10.1007\/3-540-45931-6_25"},{"key":"18_CR22","doi-asserted-by":"publisher","unstructured":"Serban, C., Iosif, R.: An Entailment Checker for Separation Logic with Inductive Definitions. Electronic Communications of the EASST 76 (May 2019). https:\/\/doi.org\/10.14279\/tuj.eceasst.76.1073","DOI":"10.14279\/tuj.eceasst.76.1073"},{"key":"18_CR23","unstructured":"Sprenger, C., Dam, M.: A Note on Global Induction in a mu-calculus with Explicit Approximations. In: \u00c9sik, Z., Ing\u00f3lfsd\u00f3ttir, A. (eds.) Fixed Points in Computer Science, FICS 2002, Copenhagen, Denmark, 20-21 July 2002, Preliminary Proceedings. BRICS Notes Series, vol. NS-02-2, pp. 22\u201324. University of Aarhus (2002), https:\/\/www.brics.dk\/NS\/02\/2\/"},{"key":"18_CR24","doi-asserted-by":"publisher","unstructured":"Ta, Q., Le, T.C., Khoo, S., Chin, W.: Automated Mutual Explicit Induction Proof in Separation Logic. In: Fitzgerald, J.S., Heitmeyer, C.L., Gnesi, S., Philippou, A. (eds.) FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09995, pp. 659\u2013676 (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_40","DOI":"10.1007\/978-3-319-48989-6_40"},{"key":"18_CR25","doi-asserted-by":"publisher","unstructured":"Ta, Q., Le, T.C., Khoo, S., Chin, W.: Automated Lemma Synthesis in Symbolic-heap Separation Logic. Proc. ACM Program. Lang. 2(POPL), 9:1\u20139:29 (2018). https:\/\/doi.org\/10.1145\/3158097","DOI":"10.1145\/3158097"},{"key":"18_CR26","doi-asserted-by":"publisher","unstructured":"Tarjan, R.: Depth-first Search and Linear Graph Algorithms. SIAM Journal on Computing 1(2), 146\u2013160 (Jun 1972). https:\/\/doi.org\/10.1137\/0201010","DOI":"10.1137\/0201010"},{"key":"18_CR27","doi-asserted-by":"publisher","unstructured":"Tellez, G., Brotherston, J.: Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. J. Autom. Reason. 64(3), 555\u2013578 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09532-0","DOI":"10.1007\/s10817-019-09532-0"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90643-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:08:08Z","timestamp":1745993288000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90643-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906428","9783031906435"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90643-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}