{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T04:51:46Z","timestamp":1775710306658,"version":"3.50.1"},"reference-count":115,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/501100001459","name":"Singapore Ministry of Education","doi-asserted-by":"crossref","award":["MOE-MOET32021-0001"],"award-info":[{"award-number":["MOE-MOET32021-0001"]}],"id":[{"id":"10.13039\/501100001459","id-type":"DOI","asserted-by":"crossref"}]}],"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>Multi-modal program verification is a process of validating code against its specification using both dynamic and symbolic techniques, and proving its correctness by a combination of automated and interactive machine-assisted tools. In order to be trustworthy, such verification tools must themselves come with formal soundness proofs, establishing that any program verified in them against a certain specification does not violate the specification's statement when executed. Verification tools that are proven sound in a general-purpose proof assistant with a small trusted core are commonly referred to as foundational.<\/jats:p>\n                  <jats:p>We present a framework that facilitates and streamlines construction of program verifiers that are both foundational and multi-modal. Our approach adopts the well-known idea of monadic shallow embedding of an executable program semantics into the programming language of a theorem prover based on higher-order logic, in our case, the Lean proof assistant. We provide a library of monad transformers for such semantics, encoding a variety of computational effects, including state, divergence, exceptions, and non-determinism. The key theoretical innovation of our work are monad transformer algebras that enable automated derivation of the respective sound verification condition generators. We show that proofs of the resulting verification conditions enjoy automation using off-the-shelf SMT solvers and allow for an interactive proof mode when automation fails. To demonstrate versatility of our framework, we instantiated it to embed two foundational multi-modal verifiers into Lean for reasoning about (1) distributed protocol safety and (2) Dafny-style specifications of imperative programs, and used them to mechanically verify a number of non-trivial case studies.<\/jats:p>","DOI":"10.1145\/3776719","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"2233-2264","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Foundational Multi-Modal Program Verifiers"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9233-3133","authenticated-orcid":false,"given":"Vladimir","family":"Gladshtein","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-5378-2815","authenticated-orcid":false,"given":"George","family":"P\u00eerlea","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1017-1562","authenticated-orcid":false,"given":"Qiyuan","family":"Zhao","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-9614-8892","authenticated-orcid":false,"given":"Vitaly","family":"Kurin","sequence":"additional","affiliation":[{"name":"Neapolis University Pafos, Paphos, Cyprus"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4250-5392","authenticated-orcid":false,"given":"Ilya","family":"Sergey","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.4153\/CJM-1961-007-5"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.16"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000137"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Danel Ahman Catalin Hritcu Kenji Maillard Guido Mart\u00ednez Gordon D. Plotkin Jonathan Protzenko Aseem Rastogi and Nikhil Swamy. 2017. Dijkstra Monads for Free. 515\u2013529. https:\/\/doi.org\/10.1145\/3009837.3009878 10.1145\/3009837.3009878","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel. 2022. Coq\u2019s Vibrant Ecosystem for Verification Engineering (Invited Talk). In CPP. ACM 2\u201311. https:\/\/doi.org\/10.1145\/3497775.3503951 10.1145\/3497775.3503951","DOI":"10.1145\/3497775.3503951"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863581"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.369.2"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Yves Bertot and Vladimir Komendantsky. 2008. Fixed point semantics and partial recursion in Coq. In PPDP. ACM 89\u201396. https:\/\/doi.org\/10.1145\/1389449.1389461 10.1145\/1389449.1389461","DOI":"10.1145\/1389449.1389461"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","unstructured":"Denis Bogdanas and Grigore Rosu. 2015. K-Java: A Complete Semantics of Java. In POPL. ACM 445\u2013456. https:\/\/doi.org\/10.1145\/2676726.2676982 10.1145\/2676726.2676982","DOI":"10.1145\/2676726.2676982"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Marcel B\u00f6hme Van-Thuan Pham and Abhik Roychoudhury. 2016. Coverage-based Greybox Fuzzing as Markov Chain. In CCS. ACM 1032\u20131043. https:\/\/doi.org\/10.1145\/2976749.2978428 10.1145\/2976749.2978428","DOI":"10.1145\/2976749.2978428"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST62969.2025.10988954"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10828-9_61"},{"key":"e_1_2_1_15_1","volume-title":"Engler","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI. USENIX Association, 209\u2013224. http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408998"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Haogang Chen Daniel Ziegler Tej Chajed Adam Chlipala M. Frans Kaashoek and Nickolai Zeldovich. 2015. Using Crash Hoare logic for certifying the FSCQ file system. In SOSP. ACM 18\u201337. https:\/\/doi.org\/10.1145\/2815400.2815402 10.1145\/2815400.2815402","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_23"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Koen Claessen and John Hughes. 2000. QuickCheck: a lightweight tool for random testing of Haskell programs. In ICFP. ACM 268\u2013279. https:\/\/doi.org\/10.1145\/351240.351266 10.1145\/351240.351266","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","unstructured":"Arthur Correnson and Dominic Steinh\u00f6fel. 2023. Engineering a Formally Verified Automated Bug Finder. In ESEC\/FSE. ACM 1165\u20131176. https:\/\/doi.org\/10.1145\/3611643.3616290 10.1145\/3611643.3616290","DOI":"10.1145\/3611643.3616290"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656437"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704856"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_27_1","unstructured":"Mike Dodds. 2024. N things I learned trying to do formal methods in industry. Available at https:\/\/mikedodds.github.io\/files\/talks\/2024-10-09-n-things-I-learned.pdf"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/Correctness49594.2019.00010"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_18"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Chucky Ellison and Grigore Rosu. 2012. An executable formal semantics of C with applications. In POPL. ACM 533\u2013544. https:\/\/doi.org\/10.1145\/2103656.2103719 10.1145\/2103656.2103719","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00005"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","unstructured":"Andrzej Filinski. 2010. Monads in action. In POPL. ACM 483\u2013494. https:\/\/doi.org\/10.1145\/1706299.1706354 10.1145\/1706299.1706354","DOI":"10.1145\/1706299.1706354"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290376"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48754-9_17"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","unstructured":"Vladimir Gladshtein Qiyuan P\u00eerlea George Zhao Vitaly Kurin and Ilya Sergey. 2025. : A Framework for Foundational Multi-Modal Program Verifiers (Artifact). https:\/\/doi.org\/10.5281\/zenodo.17347734 Working repository available at 10.5281\/zenodo.17347734","DOI":"10.5281\/zenodo.17347734"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656403"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591221"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Niklas Grimm Kenji Maillard C\u00e9dric Fournet Catalin Hritcu Matteo Maffei Jonathan Protzenko Tahina Ramananandro Aseem Rastogi Nikhil Swamy and Santiago Zanella-B\u00e9guelin. 2018. A monadic framework for relational verification: applied to information security program equivalence and optimizations. In CPP. ACM 130\u2013145. https:\/\/doi.org\/10.1145\/3167090 10.1145\/3167090","DOI":"10.1145\/3167090"},{"key":"e_1_2_1_41_1","volume-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels","author":"Gu Ronghui","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In OSDI. USENIX Association, 653\u2013669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622823"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","unstructured":"Chris Hathhorn Chucky Ellison and Grigore Rosu. 2015. Defining the undefinedness of C. In PLDI. ACM 336\u2013345. https:\/\/doi.org\/10.1145\/2737924.2737979 10.1145\/2737924.2737979","DOI":"10.1145\/2737924.2737979"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","unstructured":"Chris Hawblitzel Jon Howell Manos Kapritsos Jacob R. Lorch Bryan Parno Michael L. Roberts Srinath T. V. Setty and Brian Zill. 2015. IronFleet: proving practical distributed systems correct. In SOSP. ACM 1\u201317. https:\/\/doi.org\/10.1145\/2815400.2815428 10.1145\/2815400.2815428","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00022"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","unstructured":"Ralf Hinze. 2000. Deriving backtracking monad transformers. In ICFP. ACM 186\u2013197. https:\/\/doi.org\/10.1145\/351240.351258 10.1145\/351240.351258","DOI":"10.1145\/351240.351258"},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the First Workshop on Dafny.","author":"Ho Son","year":"2024","unstructured":"Son Ho and Cl\u00e9ment Pit-Claudel. 2024. Incremental Proof Development in Dafny with Module-Based Induction. In Proceedings of the First Workshop on Dafny."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_50_1","volume-title":"The Iris 4.3 Reference. https:\/\/iris-project.org\/ Online","author":"Project The Iris","year":"2025","unstructured":"The Iris Project. 2024. The Iris 4.3 Reference. https:\/\/iris-project.org\/ Online; last accessed 8 July 2025"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","unstructured":"Shin-ya Katsumata. 2014. Parametric effect monads and semantics of effect systems. In POPL. ACM 633\u2013646. https:\/\/doi.org\/10.1145\/2535838.2535846 10.1145\/2535838.2535846","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH58626.2023.00021"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","unstructured":"Oleg Kiselyov Chung-chieh Shan Daniel P. Friedman and Amr Sabry. 2005. Backtracking interleaving and terminating monad transformers: (functional pearl). In ICFP. ACM 192\u2013203. https:\/\/doi.org\/10.1145\/1086365.1086390 10.1145\/1086365.1086390","DOI":"10.1145\/1086365.1086390"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133901"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","unstructured":"Gerwin Klein Kevin Elphinstone Gernot Heiser June Andronick David Cock Philip Derrin Dhammika Elkaduwe Kai Engelhardt Rafal Kolanski Michael Norrish Thomas Sewell Harvey Tuch and Simon Winwood. 2009. seL4: formal verification of an OS kernel. In SOSP. ACM 207\u2013220. https:\/\/doi.org\/10.1145\/1629575.1629596 10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591268"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive Proofs in Higher-Order Concurrent Separation Logic. In POPL. ACM 205\u2013217. https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","unstructured":"Ramana Kumar Magnus O. Myreen Michael Norrish and Scott Owens. 2014. CakeML: a verified implementation of ML. In POPL. ACM 179\u2013192. https:\/\/doi.org\/10.1145\/2535838.2535841 10.1145\/2535838.2535841","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3694715.3695952"},{"key":"e_1_2_1_60_1","volume-title":"Plausible: A property testing framework for Lean 4. https:\/\/github.com\/leanprover-community\/plausible Last accessed on","year":"2025","unstructured":"leanprover-community. 2025. Plausible: A property testing framework for Lean 4. https:\/\/github.com\/leanprover-community\/plausible Last accessed on 9 July 2025"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IPL.2004.10.015"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.29007\/RKXM"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02928-9_4"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_5"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","unstructured":"Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In POPL. ACM 42\u201354. https:\/\/doi.org\/10.1145\/1111037.1111042 10.1145\/1111037.1111042","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00165-020-00523-2"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_39"},{"key":"e_1_2_1_70_1","volume-title":"Ports","author":"Li Jialin","year":"2016","unstructured":"Jialin Li, Ellis Michael, Naveen Kr. Sharma, Adriana Szekeres, and Dan R. K. Ports. 2016. Just Say NO to Paxos Overhead: Replacing Consensus with Network Ordering. In OSDI. USENIX Association, 467\u2013483. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/li"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575671"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586029"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622849"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341708"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","unstructured":"The mathlib Community. 2020. The Lean mathematical library. In CPP. ACM 367\u2013381. https:\/\/doi.org\/10.1145\/3372885.3373824 Available at 10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_12"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-98682-6_11"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","unstructured":"Oded Padon Kenneth L. McMillan Aurojit Panda Mooly Sagiv and Sharon Shoham. 2016. Ivy: safety verification by interactive generalization. In PLDI. ACM 614\u2013630. https:\/\/doi.org\/10.1145\/2908080.2908118 10.1145\/2908080.2908118","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","unstructured":"Daejun Park Andrei Stefanescu and Grigore Rosu. 2015. KJS: a complete formal semantics of JavaScript. In PLDI. ACM 346\u2013356. https:\/\/doi.org\/10.1145\/2737924.2737991 10.1145\/2737924.2737991","DOI":"10.1145\/2737924.2737991"},{"key":"e_1_2_1_85_1","unstructured":"Arthur Paulino Damiano Testa Edward Ayers Evgenia Karunus Henrik B\u00f6vinga Jannis Limperg Siddhartha Gadgil and Siddharth Bhat. 2024. Metaprogramming in Lean 4. Available at https:\/\/leanprover-community.github.io\/lean4-metaprogramming-book\/"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-98682-6_2"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00114"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-98682-6_10"},{"key":"e_1_2_1_90_1","unstructured":"Aseem Rastogi Guido Mart\u00ednez Aymeric Fromherz Tahina Ramananandro and Nikhil Swamy. 2020. Programming and Proving with Indexed Effects. https:\/\/fstar-lang.org\/papers\/indexedeffects\/indexedeffects.pdf"},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_92_1","volume-title":"The Rocq Prover. https:\/\/rocq-prover.org Version 9.0.0, released","author":"Team Rocq Development","year":"2025","unstructured":"Rocq Development Team. 2025. The Rocq Prover. https:\/\/rocq-prover.org Version 9.0.0, released March 12, 2025"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-810-5-186"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(4:28)2017"},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAP.2010.03.012"},{"key":"e_1_2_1_96_1","doi-asserted-by":"publisher","unstructured":"Michael Sammler Rodolphe Lepigre Robbert Krebbers Kayvan Memarian Derek Dreyer and Deepak Garg. 2021. RefinedC: automating the foundational verification of C code with refined ownership types. In PLDI. ACM 158\u2013174. https:\/\/doi.org\/10.1145\/3453483.3454036 10.1145\/3453483.3454036","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","unstructured":"Ilya Sergey Aleksandar Nanevski and Anindya Banerjee. 2015. Mechanized Verification of Fine-Grained Concurrent Programs. In PLDI. ACM 77\u201387. https:\/\/doi.org\/10.1145\/2737924.2737964 10.1145\/2737924.2737964","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434307"},{"key":"e_1_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"e_1_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729284"},{"key":"e_1_2_1_101_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_1_102_1","doi-asserted-by":"publisher","unstructured":"Nikhil Swamy Joel Weinberger Cole Schlesinger Juan Chen and Benjamin Livshits. 2013. Verifying Higher-Order Programs with the Dijkstra Monad. In PLDI. ACM 387\u2013398. https:\/\/doi.org\/10.1145\/2491956.2491978 10.1145\/2491956.2491978","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547640"},{"key":"e_1_2_1_104_1","volume-title":"Liquid Haskell: Haskell as a Theorem Prover. Ph. D. Dissertation","author":"Vazou Niki","year":"2016","unstructured":"Niki Vazou. 2016. Liquid Haskell: Haskell as a Theorem Prover. Ph. D. Dissertation. University of California, San Diego, USA. http:\/\/www.escholarship.org\/uc\/item\/8dm057ws"},{"key":"e_1_2_1_105_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704847"},{"key":"e_1_2_1_106_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65630-9_4"},{"key":"e_1_2_1_107_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_2_1_109_1","volume-title":"Automated Inference of Inductive Invariants for Verifying Distributed Protocols","author":"Yao Jianan","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh. 2022. DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In OSDI. USENIX Association, 485\u2013501. https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/yao"},{"key":"e_1_2_1_110_1","volume-title":"Verifying Distributed Protocols: from Executable to Decidable","author":"Yuen Mark","unstructured":"Mark Yuen. 2022. Verifying Distributed Protocols: from Executable to Decidable. Yale-NUS College. Singapore. Accompanying code available at https:\/\/github.com\/markyuen\/tlaplus-to-ivy\/"},{"key":"e_1_2_1_111_1","doi-asserted-by":"publisher","DOI":"10.1049\/BLC2.12024"},{"key":"e_1_2_1_112_1","doi-asserted-by":"publisher","unstructured":"Qiyuan Zhao George P\u00eerlea Karolina Grzeszkiewicz Seth Gilbert and Ilya Sergey. 2024. Compositional Verification of Composite Byzantine Protocols. In CCS. ACM 34\u201348. https:\/\/doi.org\/10.1145\/3658644.3690355 10.1145\/3658644.3690355","DOI":"10.1145\/3658644.3690355"},{"key":"e_1_2_1_113_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"},{"key":"e_1_2_1_114_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649821"},{"key":"e_1_2_1_115_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(1:13)2022"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776719","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:03:22Z","timestamp":1767899002000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776719"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":115,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776719"],"URL":"https:\/\/doi.org\/10.1145\/3776719","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"}}]}}