{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T23:10:09Z","timestamp":1787094609281,"version":"build-2736575974"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2024,2,22]],"date-time":"2024-02-22T00:00:00Z","timestamp":1708560000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2024,3]]},"abstract":"<jats:p>The SPARK programming language and analyzer.<\/jats:p>","DOI":"10.1145\/3624728","type":"journal-article","created":{"date-parts":[[2024,2,22]],"date-time":"2024-02-22T16:16:20Z","timestamp":1708618580000},"page":"84-94","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Co-Developing Programs and Their Proof of Correctness"],"prefix":"10.1145","volume":"67","author":[{"given":"Roderick","family":"Chapman","sequence":"first","affiliation":[{"name":"Amazon Development Centre, London, U.K"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Claire","family":"Dross","sequence":"additional","affiliation":[{"name":"AdaCore, \u00cele-de-France, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stuart","family":"Matthews","sequence":"additional","affiliation":[{"name":"Capgemini Engineering, Bath, U.K"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yannick","family":"Moy","sequence":"additional","affiliation":[{"name":"AdaCore, \u00cele-de-France, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,2,22]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"619","article-title":"Theory becoming practice","volume":"13","author":"Abrial J.","year":"2007","unstructured":"Abrial, J. Formal methods: Theory becoming practice. J. Univers. Comput. Sci. 13 (2007), 619--628.","journal-title":"J. Univers. Comput. Sci."},{"key":"e_1_2_1_2_1","unstructured":"AdaCore. A Concrete Example: A Sort Algorithm (2023); https:\/\/bit.ly\/41KawzQ"},{"key":"e_1_2_1_3_1","unstructured":"AdaCore. Managing Assumptions (2023); https:\/\/bit.ly\/41RDX35"},{"key":"e_1_2_1_4_1","unstructured":"AdaCore. SPARK Reference Manual (2023); https:\/\/bit.ly\/3TIsDEx"},{"key":"e_1_2_1_5_1","unstructured":"AdaCore and NVIDIA. Case Study (2022); https:\/\/bit.ly\/4aKXvKo"},{"key":"e_1_2_1_6_1","unstructured":"AdaCore. Tokeneer (2008); https:\/\/www.adacore.com\/tokeneer"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3470569"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of Boogie 2011: First Intern. Workshop on Intermediate Verification Languages","author":"Bobot F.","year":"2011","unstructured":"Bobot, F. et al. Why3: Shepherd your herd of provers. In Proceedings of Boogie 2011: First Intern. Workshop on Intermediate Verification Languages (2011), 53--64; https:\/\/hal.inria.fr\/hal-00790310"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0314-5"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/255471.255563"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.9"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_16"},{"key":"e_1_2_1_15_1","unstructured":"Chapman R. SPARKNaCl GitHub project (2020); https:\/\/bit.ly\/48CPsgR"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_2"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the Intern. Workshop on Satisfiability Modulo Theories (2018)","author":"Conchon S.","year":"1960","unstructured":"Conchon, S., Coquereau, A., Iguernlala, M., and Mebsout, A. Alt-Ergo 2.2. In Proceedings of the Intern. Workshop on Satisfiability Modulo Theories (2018); https:\/\/hal.inria.fr\/hal-01960203"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2018.05.003"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_20_1","first-page":"76","article-title":"Climbing the software assurance ladder---Practical formal verification for reliable software","author":"Dross C.","year":"2018","unstructured":"Dross, C. et al. Climbing the software assurance ladder---Practical formal verification for reliable software. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 76 (2018).","journal-title":"Electron. Commun. Eur. Assoc. Softw. Sci. Technol."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_5"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2187671.2187678"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/602382.602403"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3418295"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.879807"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230627"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/MIS.2004.74"},{"key":"e_1_2_1_31_1","volume-title":"The MIT Press","author":"Leino K.R.M.","year":"2023","unstructured":"Leino, K.R.M. Program Proofs. The MIT Press (2023)."},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the Usable Verification Workshop","author":"Leino K.R.M.","year":"2010","unstructured":"Leino, K.R.M. and Moskal, M. Usable auto-active verification. In Proceedings of the Usable Verification Workshop (2010)."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2017.4121212"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Limoncelli T.A. Automation should be like Iron Man not Ultron. ACM Queue (2015); https:\/\/bit.ly\/3voiz9D","DOI":"10.1145\/2844546"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.338.12"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Moy Y. Proving the Correctness of GNAT Light Runtime Library (2022); https:\/\/bit.ly\/3NQCvbk","DOI":"10.1145\/3577949.3577959"},{"key":"e_1_2_1_39_1","unstructured":"Rushby J. Formal methods and the certification of critical systems. Technical Report (1993)."},{"key":"e_1_2_1_40_1","unstructured":"Zhao Y. San\u00e1n D. Zhang F. and Liu Y. High-assurance separation kernels: A survey on formal methods. CoRR abs\/1701.01535 (2017); http:\/\/arxiv.org\/abs\/1701.01535"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3624728","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3624728","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T18:25:30Z","timestamp":1755973530000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3624728"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,2,22]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,3]]}},"alternative-id":["10.1145\/3624728"],"URL":"https:\/\/doi.org\/10.1145\/3624728","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,2,22]]},"assertion":[{"value":"2024-02-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}