{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:04:39Z","timestamp":1750309479877,"version":"3.41.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"7","license":[{"start":{"date-parts":[[2024,8,26]],"date-time":"2024-08-26T00:00:00Z","timestamp":1724630400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANRT Convention Cifre","award":["2020\/0380"],"award-info":[{"award-number":["2020\/0380"]}]},{"name":"TinyPART"},{"name":"MESRI-BMBF German-French cybersecurity program","award":["ANR-20-CYAL-0005, and 16KIS1395K"],"award-info":[{"award-number":["ANR-20-CYAL-0005, and 16KIS1395K"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2024,9,30]]},"abstract":"<jats:p>Despite growing efforts and encouraging successes in recent decades, fully formally verified projects are still rare in the industrial landscape. The industry often lacks the tools and methodologies to efficiently scale the proof development process. In this work, we give a comprehensible overview of the proof development process for proof developers and project managers. The goal is to support proof developers by rationalizing the proof development process, which currently relies heavily on their intuition and expertise, and by facilitating communication with the management line. To this end, we concentrate on the aspect of proof manufacturing and highlight the most significant sources of proof effort. We propose means to mitigate the latter through proof practices (proof structuring, proof strategies, and proof planning), proof metrics, and tools. Our approach is project-agnostic, independent of specific proof expertise, and computed estimations do not assume prior similar developments. We evaluate our guidelines using a separation kernel undergoing formal verification, driving the proof process in an optimised way. Feedback from a project manager unfamiliar with proof development confirms the benefits of detailed planning of the proof development steps, clear progress communication to the hierarchy line, and alignment with established practices in the software industry.<\/jats:p>","DOI":"10.1145\/3664807","type":"journal-article","created":{"date-parts":[[2024,6,4]],"date-time":"2024-06-04T11:37:01Z","timestamp":1717501021000},"page":"1-50","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Code to Qed, the Project Manager's Guide to Proof Engineering"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2802-0922","authenticated-orcid":false,"given":"Nicolas","family":"Dejon","sequence":"first","affiliation":[{"name":"Orange Innovation Ch\u00e2tillon, Chatillon, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5768-7665","authenticated-orcid":false,"given":"Chrystel","family":"Gaber","sequence":"additional","affiliation":[{"name":"SESAME, Orange Innovation Ch\u00e2tillon, Chatillon, France"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2117-3779","authenticated-orcid":false,"given":"Gilles","family":"Grimaud","sequence":"additional","affiliation":[{"name":"CRIStAL\/2XS, University of Lille, Lille, France"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-9694-1242","authenticated-orcid":false,"given":"Narjes","family":"Jomaa","sequence":"additional","affiliation":[{"name":"CRIStAL\/2XS, Universit\u00e9 de Lille, Lille, France"}]}],"member":"320","published-online":{"date-parts":[[2024,8,26]]},"reference":[{"key":"e_1_3_3_2_2","unstructured":"Alloy Team Members. 2021. Website of Alloy Analyzer. Retrieved December 7 2023 from https:\/\/alloytools.org\/"},{"key":"e_1_3_3_3_2","unstructured":"Kent Beck James Grenning Robert C. Martin Mike Beedle Jim Highsmith Steve Mellor Arie van Bennekum Andrew Hunt Ken Schwaber Alistair Cockburn Ron Jeffries Jeff Sutherland Ward Cunningham Jon Kern Dave Thomas Martin Fowler and Brian Marick. 2001. Website of Manifesto for Agile Software Development. Retrieved December 7 2023 from https:\/\/agilemanifesto.org\/"},{"key":"e_1_3_3_4_2","unstructured":"Leslie Lamport. 2022. Website of TLA+ Tools. Retrieved December 7 2023 from https:\/\/lamport.azurewebsites.net\/tla\/tools.html"},{"key":"e_1_3_3_5_2","unstructured":"Why3 Development Team. 2023. Website of Why3. Retrieved December 7 2023 from https:\/\/why3.lri.fr\/"},{"key":"e_1_3_3_6_2","unstructured":"University of Cambridge and Technische Universit\u00e4t M\u00fcnchen. 2022. Isabelle. Retrieved October 10 2022 from https:\/\/isabelle.in.tum.de\/index.html"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1504\/ijes.2006.014859"},{"key":"e_1_3_3_8_2","doi-asserted-by":"crossref","unstructured":"June Andronick. 2022. Website of CPP Keynote \u201cThe seL4 Verification: The Art and Craft of Proof and the Reality of Commercial Support.\u201d Retrieved June 28 2023 from https:\/\/popl22.sigplan.org\/details\/CPP-2022-papers\/27\/The-seL4-verification-the-art-and-craft-of-proof-and-the-reality-of-commercial-suppo","DOI":"10.1145\/3497775.3505265"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227120"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_3_3_11_2","first-page":"109","article-title":"Improving software development using scrum model by analyzing up and down movements on the sprint burn down chart\u2014Proposition for better alternatives","volume":"3","author":"Arafeen Md. Junaid","year":"2009","unstructured":"Md. Junaid Arafeen and Saugata Bose. 2009. Improving software development using scrum model by analyzing up and down movements on the sprint burn down chart\u2014Proposition for better alternatives. J. Digit. Content Technol. Appl. 3 (2009), 109\u2013115. Retrieved from https:\/\/api.semanticscholar.org\/CorpusID:32851875","journal-title":"J. Digit. Content Technol. Appl."},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49665-7_19"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.86.5"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31374-5_3"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359106"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.5121\/csit.2022.122309"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.5121\/ijesa.2023.13201"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048113"},{"key":"e_1_3_3_19_2","first-page":"653","article-title":"CertiKOS: An extensible architecture for building certified concurrent OS kernels","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201916). 653\u2013669.","journal-title":"Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201916)"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47846-3_14"},{"key":"e_1_3_3_23_2","unstructured":"INRIA. 1984. Website of Coq. Retrieved January 17 2020 from https:\/\/coq.inria.fr"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2014.11.005"},{"key":"e_1_3_3_25_2","volume-title":"Le co-design d'un noyau de syst\u00e8me d'exploitation et de sa preuve formelle d'isolation","author":"Jomaa Narjes","year":"2018","unstructured":"Narjes Jomaa. 2018. Le co-design d'un noyau de syst\u00e8me d'exploitation et de sa preuve formelle d'isolation. Ph.D. Dissertation. Universit\u00e9 de Lille, B\u00e2timent Esprit, Villeneuve d'Ascq."},{"key":"e_1_3_3_26_2","unstructured":"Narjes Jomaa David Nowak and Paolo Torrini. 2018. Formal Development of the Pip Protokernel. Retrieved October 10 2022 from https:\/\/entropy2018.sciencesconf.org\/data\/pip.pdf"},{"key":"e_1_3_3_27_2","article-title":"Proof-oriented design of a separation kernel with minimal trusted computing base proof-oriented design of a separation kernel with minimal trusted computing base","author":"Jomaa Narjes","year":"2019","unstructured":"Narjes Jomaa, Paolo Torrini, David Nowak, Gilles Grimaud, and Samuel Hym. 2019. Proof-oriented design of a separation kernel with minimal trusted computing base proof-oriented design of a separation kernel with minimal trusted computing base. In Proceedings of the 18th International Workshop on Automated Verification of Critical Systems (AVoCS\u201918).","journal-title":"Proceedings of the 18th International Workshop on Automated Verification of Critical Systems (AVoCS\u201918)"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_3_31_2","article-title":"ProvenCore: Towards a verified isolation micro-kernel","author":"Lescuyer Stephane","year":"2015","unstructured":"Stephane Lescuyer. 2015. ProvenCore: Towards a verified isolation micro-kernel. In Proceedings of the International Workshop on MILS: Architecture and Assurance for Secure Systems.","journal-title":"Proceedings of the International Workshop on MILS: Architecture and Assurance for Secure Systems"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.85"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3211968"},{"key":"e_1_3_3_34_2","unstructured":"Proofcraft. 2023. Website of Proofcraft. Retrieved June 28 2023 from https:\/\/proofcraft.systems\/"},{"key":"e_1_3_3_35_2","unstructured":"ProvenRun. 2020. Website of ProvenRun. Retrieved June 28 2023 from https:\/\/www.provenrun.com\/"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.2172\/1166644"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.5555\/AAI28546929"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1561\/2500000045"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/800216.806586"},{"key":"e_1_3_3_40_2","first-page":"1","volume-title":"Proceedings of the USENIX Annual Technical Conference (USENIX ATC\u201917)","author":"Sigurbjarnarson Helgi","year":"2017","unstructured":"Helgi Sigurbjarnarson, James Bornholt, Nicolas Christin, and Lorrie Faith Cranor. 2017. Push-button verification of file systems via crash refinement. In Proceedings of the USENIX Annual Technical Conference (USENIX ATC\u201917), Dilma Da Silva and Bryan Ford (Eds.). USENIX Association, 1\u201316. Retrieved from https:\/\/www.usenix.org\/conference\/atc17\/technical-sessions\/presentation\/sigurbjarnarson"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/2652524.2652551"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/CONISOFT52520.2021.00023"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSSP.2012.6225979"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3664807","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3664807","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:17:29Z","timestamp":1750295849000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3664807"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,26]]},"references-count":43,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2024,9,30]]}},"alternative-id":["10.1145\/3664807"],"URL":"https:\/\/doi.org\/10.1145\/3664807","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2024,8,26]]},"assertion":[{"value":"2023-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-05-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-26","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}