{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T06:47:39Z","timestamp":1767768459812,"version":"3.48.0"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032137104","type":"print"},{"value":"9783032137111","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-13711-1_1","type":"book-chapter","created":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T06:41:34Z","timestamp":1767768094000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Methodology for Modular Termination Verification"],"prefix":"10.1007","author":[{"given":"K. Rustan M.","family":"Leino","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Ahmadi, R., Leino, K.R.M., Nummenmaa, J.: Automatic verification of Dafny programs with traits. In: Monahan, R. (ed.) Formal Techniques for Java-like Programs, FTfJP 2015. ACM (2015)","DOI":"10.1145\/2786536.2786542"},{"issue":"3","key":"1_CR2","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/3624728","volume":"67","author":"R Chapman","year":"2024","unstructured":"Chapman, R., Dross, C., Matthews, S., Moy, Y.: Co-developing programs and their proof of correctness. Commun. ACM 67(3), 84\u201394 (2024)","journal-title":"Commun. ACM"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Schwartzbach, M.I., Ball, T. (eds.) Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, pp. 415\u2013426. ACM (2006)","DOI":"10.1145\/1133981.1134029"},{"key":"1_CR4","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ (1976)"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2014where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proceedings Symposium on Applied Mathematics, vol. 19, pp. 19\u201331 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"1_CR7","unstructured":"Jacobs, B., Bosnacki, D., Kuiper, R.: Modular termination verification. In: Boyland, J.T. (ed.) 29th European Conference on Object-Oriented Programming, ECOOP 2015. LIPIcs, vol. 37, pp. 664\u2013688. Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik (2015)"},{"key":"1_CR8","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical report CW-520, Department of Computer Science, Katholieke Universiteit Leuven, Belgium, August 2008"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, 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":"1_CR10","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Accessible software verification with Dafny. IEEE Softw. 34(6), 94\u201397 (2017)","DOI":"10.1109\/MS.2017.4121212"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"}],"container-title":["Lecture Notes in Computer Science","On the Pursuit of Insight and Elegance"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-13711-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T06:41:36Z","timestamp":1767768096000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-13711-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032137104","9783032137111"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-13711-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"8 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}