{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:42:10Z","timestamp":1767919330641,"version":"3.49.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2313998"],"award-info":[{"award-number":["2313998"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Science Foundation","award":["2513872"],"award-info":[{"award-number":["2513872"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>The Message Passing Interface (MPI) is widely used in parallel, high-performance programming, yet writing bug-free software that uses MPI remains difficult. We introduce DafnyMPI, a novel, scalable approach to formally verifying MPI software. DafnyMPI allows proving deadlock freedom, termination, and functional equivalence with simpler sequential implementations. In contrast to existing specialized frameworks, DafnyMPI avoids custom concurrency logics and instead relies on Dafny, a verification-ready programming language used for sequential programs, extending it with concurrent reasoning abilities. DafnyMPI is implemented as a library that enables safe MPI programming by requiring users to specify the communication topology upfront and to verify that calls to communication primitives such as MPI_ISEND and MPI_WAIT meet their preconditions. We formalize DafnyMPI using a core calculus and prove that the preconditions suffice to guarantee deadlock freedom. Functional equivalence is proved via rely-guarantee reasoning over message payloads and a system that guarantees safe use of read and write buffers. Termination and the absence of runtime errors are proved using standard Dafny techniques. To further demonstrate the applicability of DafnyMPI, we verify numerical solutions to three canonical partial differential equations. We believe DafnyMPI demonstrates how to make formal verification viable for a broader class of programs and provides proof engineers with additional tools for software verification of parallel and concurrent systems.<\/jats:p>","DOI":"10.1145\/3776705","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1820-1846","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0810-1941","authenticated-orcid":false,"given":"Aleksandr","family":"Fedchin","sequence":"first","affiliation":[{"name":"Tufts University, Medford, USA"},{"name":"American University of Central Asia, Bishkek, Kirghizstan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-8124-467X","authenticated-orcid":false,"given":"Antero","family":"Mejr","sequence":"additional","affiliation":[{"name":"Tufts University, Medford, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9001-5107","authenticated-orcid":false,"given":"Hari","family":"Sundar","sequence":"additional","affiliation":[{"name":"Tufts University, Medford, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8043-1166","authenticated-orcid":false,"given":"Jeffrey S.","family":"Foster","sequence":"additional","affiliation":[{"name":"Tufts University, Medford, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_13"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_9"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_32"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00166"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377812.3382144"},{"key":"e_1_2_1_7_1","volume-title":"Dafny 2024 - POPL","author":"Cutler Joseph W.","year":"2024","unstructured":"Joseph W. Cutler, Michael Hicks, and Emina Torlak. 2024. Improving the Stability of Type Safety Proofs in Dafny. In Dafny 2024 - POPL 2024. https:\/\/popl24.sigplan.org\/details\/dafny-2024-papers\/3\/Improving-the-Stability-of-Type-Safety-Proofs-in-Dafny"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.17654850"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3095075"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-72308-2_7"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_5"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_15"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373096"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571229"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632889"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2015.396"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_16"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2017.4121212"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_22"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385971"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127024.3127032"},{"key":"e_1_2_1_25_1","volume-title":"Dafny 2024 - POPL","author":"McLaughlin Sean","year":"2024","unstructured":"Sean McLaughlin, Georges-Axel Jaloyan, Tongtong Xiang, and Florian Rabe. 2024. Enhancing Proof Stability. In Dafny 2024 - POPL 2024. https:\/\/popl24.sigplan.org\/details\/dafny-2024-papers\/14\/Enhancing-Proof-Stability"},{"key":"e_1_2_1_26_1","volume-title":"MPI: A Message-Passing Interface Standard Version 1.0. https:\/\/www.mpi-forum.org\/docs\/mpi-1.0\/mpi-10.ps Accessed: 2025-05-04","author":"Interface Forum Message Passing","year":"1994","unstructured":"Message Passing Interface Forum. 1994. MPI: A Message-Passing Interface Standard Version 1.0. https:\/\/www.mpi-forum.org\/docs\/mpi-1.0\/mpi-10.ps Accessed: 2025-05-04"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","unstructured":"Salman Pervez Ganesh Gopalakrishnan Robert M Kirby Robert Palmer Rajeev Thakur and William Gropp. 2007. Practical Model-Checking Method for Verifying Correctness of MPI Programs. In Recent Advances in Parallel Virtual Machine and Message Passing Interface: 14th European PVM\/MPI User\u2019s Group Meeting. 344\u2013353. https:\/\/doi.org\/10.1007\/978-3-540-75416-9_46 10.1007\/978-3-540-75416-9_46","DOI":"10.1007\/978-3-540-75416-9_46"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1941553.1941603"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE58978.2023.00017"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409003"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87475-1_34"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1345206.1345258"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2010.7"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594835.1504214"},{"key":"e_1_2_1_35_1","unstructured":"Large MPI Tags with the Intel MPI Library. 2025. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/large-mpi-tags-with-the-intel-mpi.html Accessed: 2025-04-12"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776705","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:05:43Z","timestamp":1767899143000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776705"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":35,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776705"],"URL":"https:\/\/doi.org\/10.1145\/3776705","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}