{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T13:55:35Z","timestamp":1746194135422,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031384981"},{"type":"electronic","value":"9783031384998"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>There are many techniques and tools to prove termination of  programs, but up to now these tools were not very powerful for fully automated termination proofs of programs whose termination depends on recursive data structures like lists. We present the first approach that extends powerful techniques for termination analysis of  programs (with memory allocation and explicit pointer arithmetic) to lists.<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_16","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"266-285","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Proving Termination of\u00a0C Programs with\u00a0Lists"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2852-9830","authenticated-orcid":false,"given":"Jera","family":"Hensel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0283-8520","authenticated-orcid":false,"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/11817963_35","volume-title":"Computer Aided Verification","author":"J Berdine","year":"2006","unstructured":"Berdine, J., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 386\u2013400. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_35"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Progress on software verification: SV-COMP 2022. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13244, pp. 375\u2013402. Springer, Cham (2022). http:\/\/sv-comp.sosy-lab.org\/2022\/. https:\/\/doi.org\/10.1007\/978-3-030-99527-0_20","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Bozga, M., Iosif, R., Perarnau, S.: Quantitative separation logic and programs with lists. J. Aut. Reason. 45(2), 131\u2013156 (2010). http:\/\/dx.doi.org\/10.1007\/s10817-010-9179-9","DOI":"10.1007\/s10817-010-9179-9"},{"key":"16_CR5","unstructured":"Brockschmidt, M., Otto, C., Giesl, J.: Modular termination proofs of recursive Java Bytecode programs by term rewriting. In: Schmidt-Schauss, S. (ed.) RTA 2011, LIPIcs 10, pp. 155\u2013170 (2011). http:\/\/dx.doi.org\/10.4230\/LIPIcs.RTA.2011.155"},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Brockschmidt, M., Musiol, R., Otto, C., Giesl, J.: Automated termination proofs for Java programs with cyclic data. In: Madhusudan, P.., Seshia, Sanjit A.. (eds.) CAV 2012. LNCS, vol. 7358, pp. 105\u2013122. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_13","DOI":"10.1007\/978-3-642-31424-7_13"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-662-49674-9_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Brockschmidt","year":"2016","unstructured":"Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387\u2013393. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_22"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Chen, Y.-F., et al.: Advanced automata-based algorithms for program termination checking. In: Foster, J.S., Grossman, D. (eds.) PLDI 2018, pp. 135\u2013150 (2018). http:\/\/dx.doi.org\/10.1145\/3192366.3192405","DOI":"10.1145\/3296979.3192405"},{"key":"16_CR9","unstructured":"Clang: http:\/\/clang.llvm.org"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-662-46669-8_27","volume-title":"Programming Languages and Systems","author":"C David","year":"2015","unstructured":"David, C., Kroening, D., Lewis, M.: Propositional reasoning about safety and termination of heap-manipulating programs. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 661\u2013684. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_27"},{"key":"16_CR11","unstructured":"Emrich, F., Hensel, J., Giesl, J.: AProVE: Modular termination analysis of memory-manipulating C programs. CoRR, abs\/2302.02382 (2023). http:\/\/dx.doi.org\/10.48550\/arXiv.2302.02382"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Frohn, F., Giesl, J.: Proving non-termination via loop acceleration. In: Barrett, C.W., Yang, J. (eds.) FMCAD 2019, pp. 221\u2013230 (2019). http:\/\/dx.doi.org\/10.23919\/FMCAD.2019.8894271","DOI":"10.23919\/FMCAD.2019.8894271"},{"key":"16_CR13","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Proving non-termination and lower runtime bounds with LoAT (system description). In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning. IJCAR 2022. LNCS, vol. 13385, pp. 712\u2013722. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_41","DOI":"10.1007\/978-3-031-10769-6_41"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Giesl, J., et al.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reason. 58(1), 3\u201331 (2017). http:\/\/dx.doi.org\/10.1007\/s10817-016-9389-x","DOI":"10.1007\/s10817-016-9388-y"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 156\u2013166. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_10. http:\/\/termination-portal.org\/wiki\/Termination_Competition_2022","DOI":"10.1007\/978-3-030-17502-3_10"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Hensel, J., Giesl, J., Frohn, F., Str\u00f6der, T.: Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution. J. Log. Algebr. Methods Program. 97, 105\u2013130, (2018). http:\/\/dx.doi.org\/10.1016\/j.jlamp.2018.02.004","DOI":"10.1016\/j.jlamp.2018.02.004"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-030-99527-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Hensel","year":"2022","unstructured":"Hensel, J., Mensendiek, C., Giesl, J.: AProVE: non-termination witnesses for C programs (competition contribution). In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13244, pp. 403\u2013407. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_21"},{"key":"16_CR18","unstructured":"Hensel, J., Giesl, J.: Proving termination of C programs with lists. CoRR, abs\/2305.12159 (2023). http:\/\/dx.doi.org\/10.48550\/arXiv.2305.12159"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Le, T.C., Qin, S., Chin, W.N.: Termination and non-termination specification inference. In: Grove, D., Blackburn, S.M. (eds.) PLDI 2015, pp. 489\u2013498 (2015). http:\/\/dx.doi.org\/10.1145\/2737924.2737993","DOI":"10.1145\/2813885.2737993"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-319-89963-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Mal\u00edk","year":"2018","unstructured":"Mal\u00edk, V., Marti\u010dek, \u0160, Schrammel, P., Srivas, M., Vojnar, T., Wahlang, J.: 2LS: memory safety and non-termination. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 417\u2013421. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_24"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"Metta, R., Yeduru, P., Karmarkar, H., Medicherla, R.K.: VeriFuzz 1.4: checking for (non-)termination (competition contribution). In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13994, pp. 594\u2013599. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_42","DOI":"10.1007\/978-3-031-30820-8_42"},{"key":"16_CR22","unstructured":"Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Lynch, C. (ed.) RTA 2011, LIPIcs, vol. 6, pp. 259\u2013276 (2010). http:\/\/dx.doi.org\/10.4230\/LIPIcs.RTA.2010.259"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-030-17502-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Richter","year":"2019","unstructured":"Richter, C., Wehrheim, H.: PeSCo: predicting sequential combinations of verifiers. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 229\u2013233. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_19"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Rowe, R.N.S., Brotherston, J.: Automatic cyclic termination proofs for recursive procedures in separation logic. In: Bertot, Y., Vafeiadis, V. (eds.) CPP 2017, pp. 53\u201365 (2017). http:\/\/dx.doi.org\/10.1145\/3018610.3018623","DOI":"10.1145\/3018610.3018623"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Str\u00f6der, T., et al.: Automatically proving termination and memory safety for programs with pointer arithmetic. J. Autom. Reason. 58(1), 33\u201365 (2017). http:\/\/dx.doi.org\/10.1007\/s10817-016-9389-x","DOI":"10.1007\/s10817-016-9389-x"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. In: Field, J., Hicks, M. (eds.) POPL 2012, pp. 427\u2013440 (2012). http:\/\/dx.doi.org\/10.1145\/2103656.2103709","DOI":"10.1145\/2103621.2103709"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:04:53Z","timestamp":1693609493000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}