{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T06:50:26Z","timestamp":1781938226122,"version":"3.54.5"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032283573","type":"print"},{"value":"9783032283580","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-28358-0_11","type":"book-chapter","created":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T06:02:10Z","timestamp":1781935330000},"page":"216-237","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Deductive Verification of\u00a0Legal Contracts"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8000-7613","authenticated-orcid":false,"given":"Reiner","family":"H\u00e4hnle","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0052-4061","authenticated-orcid":false,"given":"Cosimo","family":"Laneve","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,21]]},"reference":[{"key":"11_CR1","unstructured":"The Accord Project: Open source software tools for smart legal contracts. https:\/\/accordproject.org. Accessed 31 Mar 2026"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification: The KeY Book. LNCS, vol. 10001. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-030-61467-6_2","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Applications","author":"W Ahrendt","year":"2020","unstructured":"Ahrendt, W., Bubel, R.: Functional verification of smart contracts via strong data integrity. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12478, pp. 9\u201324. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61467-6_2"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Beckert, B., et al.: The Java verification tool KeY: a tutorial. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds.) FM 2024. LNCS, vol. 14934, pp. 597\u2013623. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-71177-0_32","DOI":"10.1007\/978-3-031-71177-0_32"},{"key":"11_CR5","unstructured":"Beckert, B., Herda, M., Kirsten, M., Schiffl, J.: Formal specification and verification of hyperledger fabric chaincode. In: 3rd Symposium on Distributed Ledger Technology (SDLT), Gold Coast, Australia, 12 November 2018, pp. 44\u201348. Institute for Integrated and Intelligent Systems (2018)"},{"issue":"2","key":"11_CR6","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/S10009-024-00738-1","volume":"26","author":"F Cassez","year":"2024","unstructured":"Cassez, F., Fuller, J., Quiles, H.M.A.: Deductive verification of smart contracts with Dafny. Int. J. Softw. Tools Technol. Transf. 26(2), 131\u2013145 (2024). https:\/\/doi.org\/10.1007\/S10009-024-00738-1","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Cok, D.R.: JML and OpenJML for Java 16. In: Cok, D.R. (ed.) FTfJP 2021: Proceedings of 23rd ACM International Workshop on Formal Techniques for Java-like Programs, Virtual Event, Denmark, pp. 65\u201367. ACM (2021). https:\/\/doi.org\/10.1145\/3464971.3468417","DOI":"10.1145\/3464971.3468417"},{"key":"11_CR8","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2022.102911","volume":"225","author":"S Crafa","year":"2023","unstructured":"Crafa, S., Laneve, C., Sartor, G., Veschetti, A.: Pacta sunt servanda: legal contracts in Stipula. Sci. Comput. Program. 225, 102911 (2023). https:\/\/doi.org\/10.1016\/j.scico.2022.102911","journal-title":"Sci. Comput. Program."},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J-C Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173\u2013177. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_21"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11813040_9","volume-title":"FM 2006: Formal Methods","author":"A Freitas","year":"2006","unstructured":"Freitas, A., Cavalcanti, A.: Automatic translation from Circus to Java. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 115\u2013130. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11813040_9"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Laneve, C., Veschetti, A.: Formal verification of legal contracts: a translation-based approach. In: Damiani, F., Farrell, M. (eds.) IFM 2025. LNCS, vol. 16194, pp. 59\u201378. Springer, Cham (2025).https:\/\/doi.org\/10.1007\/978-3-032-10794-7_4","DOI":"10.1007\/978-3-032-10794-7_4"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Hamie, A., Haddad, H., Omicini, A., Wainwright, R.L.: Translating the object constraint language into the java modelling language. In: Liebrock, L.M. (ed.) Proceedings of the ACM Symposium on Applied Computing (SAC), pp. 1531\u20131535. ACM, Nicosia, Cyprus (2004). https:\/\/doi.org\/10.1145\/967900.968206","DOI":"10.1145\/967900.968206"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Laneve, C.: The stipula platform: a workbench for programming and analyzing legal contracts. In: Journeys Between Formal Methods and the Railway Industry: Essays Dedicated to Alessandro Fantechi on the Occasion of His 70th Birthday. LNCS, vol. 16470, pp. 160\u2013177. Springer (2026)","DOI":"10.1007\/978-3-032-12484-5_9"},{"key":"11_CR14","unstructured":"Lexon Foundation. https:\/\/gitlab.com\/lexon-foundation. Accessed 31 Mar 2026"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Merigoux, D., Chataing, N., Protzenko, J.: Catala: a programming language for the law. Proc. ACM Program. Lang. 5(ICFP), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3473582","DOI":"10.1145\/3473582"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Neha\u00ef, Z., Bobot, F.: Deductive proof of industrial smart contracts using why3. In: Sekerinski, E., et al. (eds.) FM 2019. LNCS, vol. 12232, pp. 299\u2013311. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-54994-7_22","DOI":"10.1007\/978-3-030-54994-7_22"},{"key":"11_CR17","unstructured":"Obsidian: A safer blockchain programming language. http:\/\/obsidian-lang.com\/. Accessed 31 Mar 2026"},{"key":"11_CR18","unstructured":"OpenLaw: Real world contracts for Ethereum. https:\/\/www.openlaw.io. Accessed 31 Mar 2026"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Roche, N., Hernandez, W., Chen, E., Sim\u00e9on, J., Selman, D.: Ergo \u2013 a programming language for smart legal contracts. arXiv CoRR (2021). https:\/\/doi.org\/10.48550\/arXiv.2112.07064","DOI":"10.48550\/arXiv.2112.07064"},{"key":"11_CR20","unstructured":"Solidity Documentation: State Machine Common Pattern. https:\/\/docs.soliditylang.org\/en\/v0.8.35-pre.1\/common-patterns.html#state-machine. Accessed 31 Mar 2026"},{"key":"11_CR21","unstructured":"The Stipula Project. https:\/\/github.com\/stipula-language. Accessed 31 Mar 2026"}],"container-title":["Lecture Notes in Computer Science","Coordination Models and Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-28358-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T06:02:11Z","timestamp":1781935331000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28358-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032283573","9783032283580"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28358-0_11","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":"21 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"COORDINATION","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Coordination Models and Languages","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Urbino","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":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 June 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 June 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"coordination2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2026\/coordination","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}