{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:05:46Z","timestamp":1750309546670,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,7,3]],"date-time":"2024-07-03T00:00:00Z","timestamp":1719964800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,7,3]]},"DOI":"10.1145\/3698322.3698340","type":"proceedings-article","created":{"date-parts":[[2024,12,10]],"date-time":"2024-12-10T16:46:22Z","timestamp":1733849182000},"page":"1-7","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["The Faultless Way of Programming"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9036-5692","authenticated-orcid":false,"given":"James","family":"Noble","sequence":"first","affiliation":[{"name":"creative research & programming, Wellington, Wellington, New Zealand"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3051-4195","authenticated-orcid":false,"given":"Charles","family":"Weir","sequence":"additional","affiliation":[{"name":"School of Computing and Communications, Lancaster University, Lancaster, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2024,12,10]]},"reference":[{"key":"e_1_3_3_1_2_2","unstructured":"Amazon. 2023. Automated reasoning. https:\/\/www.amazon.science\/research-areas\/automated-reasoning."},{"key":"e_1_3_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_2"},{"key":"e_1_3_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA201017"},{"key":"e_1_3_3_1_5_2","unstructured":"CompCert. 2023. CompCert. https:\/\/github.com\/AbsInt\/CompCert. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_3_1_6_2","unstructured":"Dafny. 2023. dafny-lang. https:\/\/github.com\/dafny-lang\/dafny. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_3_1_8_2","volume-title":"E.W. Dijkstra Archive: the manuscripts of Edsger W. Dijkstra","author":"Dijkstra Edsger\u00a0W.","year":"1970","unstructured":"Edsger\u00a0W. Dijkstra. 1970. On the reliability of programs (EWD303). In E.W. Dijkstra Archive: the manuscripts of Edsger W. Dijkstra. https:\/\/www.cs.utexas.edu\/users\/EWD\/"},{"key":"e_1_3_3_1_9_2","doi-asserted-by":"publisher","unstructured":"Andres Erbsen Jade Philipoom Jason Gross Robert Sloan and Adam Chlipala. 2020. Simple High-Level Code For Cryptographic Arithmetic: With Proofs Without Compromises. ACM SIGOPS Oper. Syst. Rev. 54 1 (2020) 23\u201330. 10.1145\/3421473.3421477https:\/\/dl.acm.org\/doi\/10.1145\/3421473.3421477","DOI":"10.1145\/3421473.3421477"},{"key":"e_1_3_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.PPES.2011.59"},{"key":"e_1_3_3_1_11_2","unstructured":"GCC. 2023. GCC the GNU Compiler Collection. https:\/\/gcc.gnu.org\/. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_3_1_12_2","unstructured":"C.A.R. Hoare. 2009. Null References: The Billion Dollar Mistake. Presentation to INFOQ Conference."},{"key":"e_1_3_3_1_13_2","doi-asserted-by":"publisher","unstructured":"C.\u00a0A.\u00a0R. Hoare. 1969. An Axiomatic Basis for Computer Programming. CACM 12 10 (1969) 576\u2013580. 10.1145\/363235.363259https:\/\/dl.acm.org\/doi\/10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_3_1_14_2","unstructured":"Kevin Jacobs and Benjamin Beurdouche. 2022. Performance Improvements via Formally-Verified Cryptography in Firefox. https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-viaformally-verified-cryptography-in-firefox\/. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_3_1_16_2","doi-asserted-by":"crossref","unstructured":"Claire Le\u00a0Goues K\u00a0Rustan\u00a0M Leino and Micha\u0142 Moskal. 2011. The Boogie verification debugger. SEFM LNCS 7041 (2011) 407\u2013414.","DOI":"10.1007\/978-3-642-24690-6_28"},{"key":"e_1_3_3_1_17_2","doi-asserted-by":"publisher","unstructured":"K.\u00a0Rustan\u00a0M. Leino. 2017. Accessible Software Verification with Dafny. IEEE Softw. 34 6 (2017) 94\u201397. 10.1109\/MS.2017.4121212'","DOI":"10.1109\/MS.2017.4121212"},{"key":"e_1_3_3_1_18_2","volume-title":"Program Proofs","author":"Leino K.\u00a0Rustan\u00a0M.","year":"2023","unstructured":"K.\u00a0Rustan\u00a0M. Leino. 2023. Program Proofs. MIT Press."},{"key":"e_1_3_3_1_19_2","unstructured":"LLVM. 2023. The LLVM Compiler Infrastructure. https:\/\/llvm.org\/. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_3_1_20_2","doi-asserted-by":"crossref","unstructured":"Bertrand Meyer. 1992. Applying \u2019Design by Contract\u2019. Computer 25 10 (1992) 40\u201351.","DOI":"10.1109\/2.161279"},{"key":"e_1_3_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92145-5"},{"key":"e_1_3_3_1_22_2","unstructured":"Microsoft. 2023. The Dafny Programming and Verification Language. https:\/\/dafny.org\/. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_3_1_23_2","unstructured":"Microsoft. 2023. Microsoft Research. https:\/\/www.microsoft.com\/en-us\/research\/. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3634763"},{"key":"e_1_3_3_1_25_2","volume-title":"Selected Papers on Automath","author":"Nederpelt R.P.","year":"1994","unstructured":"R.P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer (Eds.). 1994. Selected Papers on Automath. North Holland."},{"key":"e_1_3_3_1_26_2","volume-title":"Dafny Workshop at POPL","author":"Noble James","year":"2024","unstructured":"James Noble. 2024. Learn \u2019em Dafny. In Dafny Workshop at POPL (London, England). https:\/\/popl24.sigplan.org\/details\/dafny-2024-papers\/11\/Learn-em-Dafny"},{"key":"e_1_3_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_23"},{"key":"e_1_3_3_1_28_2","unstructured":"seL4 Project. 2023. The seL4\u00ae Microkernel. https:\/\/sel4.systems\/. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_9"},{"key":"e_1_3_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428296"},{"key":"e_1_3_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"event":{"name":"EuroPLoP 2024: 29th European Conference on Pattern Languages of Programs, People, and Practices","acronym":"EuroPLoP 2024","location":"Irsee Germany"},"container-title":["Proceedings of the 29th European Conference on Pattern Languages of Programs, People, and Practices"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3698322.3698340","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3698322.3698340","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:42Z","timestamp":1750295922000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3698322.3698340"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,3]]},"references-count":30,"alternative-id":["10.1145\/3698322.3698340","10.1145\/3698322"],"URL":"https:\/\/doi.org\/10.1145\/3698322.3698340","relation":{},"subject":[],"published":{"date-parts":[[2024,7,3]]},"assertion":[{"value":"2024-12-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}