{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T09:02:25Z","timestamp":1743066145365,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031765537"},{"type":"electronic","value":"9783031765544"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-76554-4_5","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T11:18:09Z","timestamp":1731410289000},"page":"75-84","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Proving Termination via\u00a0Measure Transfer in\u00a0Equivalence Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-0795-881X","authenticated-orcid":false,"given":"Dragana","family":"Milovan\u010devi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-3697-4383","authenticated-orcid":false,"given":"Carsten","family":"Fuhs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mario","family":"Bucev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7044-9522","authenticated-orcid":false,"given":"Viktor","family":"Kun\u010dak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Albert, E., Bubel, R., Genaim, S., H\u00e4hnle, R., Puebla, G., Rom\u00e1n-D\u00edez, G.: A formal verification framework for static analysis - as well as its instantiation to the resource analyzer COSTA and formal verification tool KeY. Softw. Syst. Model. 15(4), 987\u20131012 (2016). https:\/\/doi.org\/10.1007\/S10270-015-0476-Y","DOI":"10.1007\/S10270-015-0476-Y"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J. (eds.) TACAS 2016. LNCS, vol.\u00a09636, pp. 387\u2013393. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_22","DOI":"10.1007\/978-3-662-49674-9_22"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Bucev, M., Kun\u010dak, V.: Formally verified quite OK image format. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17\u201321, 2022. pp. 343\u2013348. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_41","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_41"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Burdy, L., et al.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7(3), 212\u2013232 (2005). https:\/\/doi.org\/10.1007\/S10009-004-0167-4","DOI":"10.1007\/S10009-004-0167-4"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Chassot, S., Kun\u010dak, V.: Verifying a realistic mutable hash table - case study (short paper). In: Benzm\u00fcller, C., Heule, M.J.H., Schmidt, R.A. (eds.) IJCAR 2024, Part I. LNCS, vol. 14739, pp. 304\u2013314. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_18","DOI":"10.1007\/978-3-031-63498-7_18"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Chen, Y., et al.: Advanced automata-based algorithms for program termination checking. In: Foster, J.S., Grossman, D. (eds.) Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, pp. 135\u2013150. ACM (2018). https:\/\/doi.org\/10.1145\/3192366.3192405","DOI":"10.1145\/3192366.3192405"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Hipspec: automating inductive proofs of program properties. In: Fleuriot, J.D., H\u00f6fner, P., McIver, A., Smaill, A. (eds.) ATx\u201912\/WInG\u201912: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation, Manchester, UK, June 2012. EPiC Series in Computing, vol.\u00a017, pp. 16\u201325. EasyChair (2012). https:\/\/doi.org\/10.29007\/3qwr","DOI":"10.29007\/3qwr"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Cohen, C., Crance, E., Mahboubi, A.: TROCQ: proof transfer for free, with or without univalence. In: Weirich, S. (ed.) ESOP 2024, Part I. LNCS, vol. 14576, pp. 239\u2013268. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57262-3_10","DOI":"10.1007\/978-3-031-57262-3_10"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification. In: Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering. ASE 2014, New York, NY, USA, pp. 349-360. Association for Computing Machinery (2014).https:\/\/doi.org\/10.1145\/2642937.2642987","DOI":"10.1145\/2642937.2642987"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Giesl, J., et al.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reason. 58(1), 3\u201331 (2017). https:\/\/doi.org\/10.1007\/S10817-016-9388-Y","DOI":"10.1007\/S10817-016-9388-Y"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Gopinathan, K., Keoliya, M., Sergey, I.: Mostly automated proof repair for verified libraries. Proc. ACM Program. Lang. 7(PLDI), 25\u201349 (2023). https:\/\/doi.org\/10.1145\/3591221","DOI":"10.1145\/3591221"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Hamza, J., Voirol, N., Kun\u010dak, V.: System FR: formalized foundations for the Stainless verifier. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360592","DOI":"10.1145\/3360592"},{"key":"5_CR13","unstructured":"INRIA: Functional induction in coq (2021). https:\/\/coq.inria.fr\/refman\/using\/libraries\/funind.html"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Kaufmann, M.: DefunT: a tool for automating termination proofs by using the community books (extended abstract). In: Goel, S., Kaufmann, M. (eds.) Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018. EPTCS, vol.\u00a0280, pp. 161\u2013163 (2018). https:\/\/doi.org\/10.4204\/EPTCS.280.12","DOI":"10.4204\/EPTCS.280.12"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Kop, C.: WANDA - a higher order termination tool (system description). In: Ariola, Z.M. (ed.) 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference). LIPIcs, vol.\u00a0167, pp. 36:1\u201336:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPICS.FSCD.2020.36","DOI":"10.4230\/LIPICS.FSCD.2020.36"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic termination verification for higher-order functional programs. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol.\u00a08410, pp. 392\u2013411. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_21","DOI":"10.1007\/978-3-642-54833-8_21"},{"key":"5_CR17","unstructured":"LARA, E.: Stainless (2023). https:\/\/github.com\/epfl-lara\/stainless"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, LPAR-16. LNCS, vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Mal\u00edk, V., Vojnar, T.: Automatically checking semantic equivalence between versions of large-scale C projects. In: 2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST), pp. 329\u2013339 (2021). https:\/\/doi.org\/10.1109\/ICST49551.2021.00045","DOI":"10.1109\/ICST49551.2021.00045"},{"key":"5_CR20","unstructured":"Milovancevic, D., Bucev, M., Wojnarowski, M., Chassot, S., Kuncak, V.: Formal autograding in a classroom (experience report) (2024). http:\/\/infoscience.epfl.ch\/record\/309386"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Milovan\u010devi\u0107, D., Kun\u010dak, V.: Proving and disproving equivalence of functional programming assignments. Proc. ACM Program. Lang. 7(PLDI) (2023). https:\/\/doi.org\/10.1145\/3591258","DOI":"10.1145\/3591258"},{"key":"5_CR22","unstructured":"Milovan\u010devi\u0107, D., Fuhs, C., Bucev, M., Kuncak, V.: Proving Termination via Measure Transfer in Equivalence Checking (Extended Version). Technical report, EPFL (2024). https:\/\/infoscience.epfl.ch\/handle\/20.500.14299\/241339"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Milovan\u010devi\u0107, D., Fuhs, C., Bucev, M., Kun\u010dak, V.: Proving Termination via Measure Transfer in Equivalence Checking (Artifact) (2024). https:\/\/doi.org\/10.5281\/zenodo.13787855","DOI":"10.5281\/zenodo.13787855"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic, vol.\u00a02283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"5_CR25","unstructured":"Ringer, T.: Proof Repair. Ph.D. thesis, University of Washington, USA (2021). https:\/\/hdl.handle.net\/1773\/47429"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Ringer, T., Porter, R., Yazdani, N., Leo, J., Grossman, D.: Proof repair across type equivalences. 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\u201325, 2021, pp. 112\u2013127. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454033, https:\/\/doi.org\/10.1145\/3453483.3454033","DOI":"10.1145\/3453483.3454033 10.1145\/3453483.3454033"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Sharma, R., Schkufza, E., Churchill, B., Aiken, A.: Data-driven equivalence checking. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications. OOPSLA \u201913, New York, NY, USA, pp. 391\u2013406. Association for Computing Machinery (2013). https:\/\/doi.org\/10.1145\/2509136.2509509","DOI":"10.1145\/2509136.2509509"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Strichman, O., Godlin, B.: Regression verification - a practical way to verify programs. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 496\u2013501. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-69149-5_54","DOI":"10.1007\/978-3-540-69149-5_54"},{"key":"5_CR29","doi-asserted-by":"publisher","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) SAS 2011, vol.\u00a06887, pp. 298\u2013315. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_23","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Urban, C.: FuncTion: an abstract domain functor for termination - (competition contribution). In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015. LNCS, vol.\u00a09035, pp. 464\u2013466. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_46","DOI":"10.1007\/978-3-662-46681-0_46"},{"key":"5_CR31","unstructured":"Voirol, N.: Termination Analysis in a Higher-Order Functional Context. Master\u2019s thesis, EPFL (2023). http:\/\/infoscience.epfl.ch\/record\/311772"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-76554-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T11:38:24Z","timestamp":1737200304000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-76554-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031765537","9783031765544"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-76554-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that\u00a0are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Manchester","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2024.cs.manchester.ac.uk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}