{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:17:15Z","timestamp":1760044635499,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031081651"},{"type":"electronic","value":"9783031081668"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-08166-8_6","type":"book-chapter","created":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:03:27Z","timestamp":1656889407000},"page":"105-128","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Specifying the Boundary Between Unverified and Verified Code"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1864-4974","authenticated-orcid":false,"given":"David R.","family":"Cok","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2872-8039","authenticated-orcid":false,"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,7,4]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification\u2014The KeY Book\u2014From Theory to Practice. LNCS, vol. 10001. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"issue":"6","key":"6_CR2","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1145\/1953122.1953145","volume":"54","author":"M Barnett","year":"2011","unstructured":"Barnett, M., F\u00e4hndrich, M., Leino, K.R.M., M\u00fcller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Comm. ACM 54(6), 81\u201391 (2011). https:\/\/doi.org\/10.1145\/1953122.1953145","journal-title":"Comm. ACM"},{"issue":"8","key":"6_CR3","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/3470569","volume":"64","author":"P Baudin","year":"2021","unstructured":"Baudin, P., et al.: The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Comm. ACM 64(8), 56\u201368 (2021). https:\/\/doi.org\/10.1145\/3470569","journal-title":"Comm. ACM"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/978-3-642-20398-5_35","volume-title":"NASA Formal Methods","author":"DR Cok","year":"2011","unstructured":"Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472\u2013479. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_35"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Cok, D.R.: JML and OpenJML for Java 16. In: Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2021, pp. 65\u201367. ACM (2021). https:\/\/doi.org\/10.1145\/3464971.3468417","DOI":"10.1145\/3464971.3468417"},{"key":"6_CR6","unstructured":"Cok, D.R., Leavens, G.T., Ulbrich, M.: JML Reference Manual, 2nd edn. (2021). https:\/\/www.openjml.org\/documentation\/JML_Reference_Manual.pdf"},{"key":"6_CR7","unstructured":"ECMA International: Eiffel: Analysis, Design and Programming Language, 2nd edn., June 2006. Standard ECMA-367"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Goodenough, J.B.: Structured exception handling. In: Graham, R.M., Harrison, M.A., Reynolds, J.C. (eds.) Conference Record of the Second ACM Symposium on Principles of Programming Languages, pp. 204\u2013224. ACM, January 1975. https:\/\/doi.org\/10.1145\/512976.512997","DOI":"10.1145\/512976.512997"},{"key":"6_CR9","volume-title":"The Java Language Specification","author":"J Gosling","year":"1996","unstructured":"Gosling, J., Joy, B., Steele, G.: The Java Language Specification. Addison-Wesley, Boston (1996)"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1\u201316:58 (2012). https:\/\/doi.org\/10.1145\/2187671.2187678. Article 16","DOI":"10.1145\/2187671.2187678"},{"key":"6_CR11","unstructured":"Klabnik, S., Nichols, C.: The Rust Programming Language (2018). https:\/\/doc.rust-lang.org\/book\/"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","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"},{"issue":"6","key":"6_CR13","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1109\/MS.2017.4121212","volume":"34","author":"KRM Leino","year":"2017","unstructured":"Leino, K.R.M.: Accessible software verification with Dafny. IEEE Softw. 34(6), 94\u201397 (2017). https:\/\/doi.org\/10.1109\/MS.2017.4121212","journal-title":"IEEE Softw."},{"key":"6_CR14","unstructured":"Leino, K.R.M., Ford, R.L., Cok, D.R.: Dafny reference manual (2021). https:\/\/dafny-lang.github.io\/dafny\/DafnyRef\/DafnyRef"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M., Schulte, W.: Exception safety for C#. In: Cuellar, J.R., Liu, Z. (eds.) SEFM 2004\u2013Second International Conference on Software Engineering and Formal Methods, pp. 218\u2013227. IEEE, September 2004. https:\/\/doi.org\/10.1109\/SEFM.2004.14","DOI":"10.1109\/SEFM.2004.14"},{"key":"6_CR16","series-title":"Series in Computer Science","volume-title":"Object-oriented Software Construction","author":"B Meyer","year":"1988","unstructured":"Meyer, B.: Object-oriented Software Construction. Series in Computer Science, Prentice-Hall International, Hoboken (1988)"}],"container-title":["Lecture Notes in Computer Science","The Logic of Software. A Tasting Menu of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-08166-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:38:38Z","timestamp":1656891518000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-08166-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031081651","9783031081668"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-08166-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"4 July 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}