{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T02:21:34Z","timestamp":1785291694910,"version":"3.55.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T00:00:00Z","timestamp":1680739200000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,4,6]]},"abstract":"<jats:p>Previous work on rewriting and reachability logic establishes a vision for a language-agnostic program verifier, which takes three inputs: a program, its formal specification, and the formal semantics of the programming language in which the program is written. The verifier then uses a language-agnostic verification algorithm to prove the program correct with respect to the specification and the formal language semantics. Such a complex verifier can easily have bugs. This paper proposes a method to certify the correctness of each successful verification run by generating a proof certificate. The proof certificate can be checked by a small proof checker. The preliminary experiments apply the method to generate proof certificates for program verification in an imperative language, a functional language, and an assembly language, showing that the proposed method is language-agnostic.<\/jats:p>","DOI":"10.1145\/3586029","type":"journal-article","created":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T21:06:02Z","timestamp":1680815162000},"page":"56-84","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5475-5765","authenticated-orcid":false,"given":"Zhengyao","family":"Lin","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3208-4061","authenticated-orcid":false,"given":"Xiaohong","family":"Chen","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5716-9400","authenticated-orcid":false,"given":"Minh-Thai","family":"Trinh","sequence":"additional","affiliation":[{"name":"Advanced Digital Sciences Center, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-3613-2784","authenticated-orcid":false,"given":"John","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3102-0421","authenticated-orcid":false,"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,4,6]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_2_2_1","volume-title":"Leonardo De Moura, and Pascal Fontaine","author":"Barrett Clark","year":"2015","unstructured":"Clark Barrett , Leonardo De Moura, and Pascal Fontaine . 2015 . Proofs in satisfiability modulo theories. Available at. http:\/\/leodemoura.github.io\/files\/SMTProofs.pdf All about proofs, Proofs for all, 55, 1 (2015), 23\u201344. Clark Barrett, Leonardo De Moura, and Pascal Fontaine. 2015. Proofs in satisfiability modulo theories. Available at. http:\/\/leodemoura.github.io\/files\/SMTProofs.pdf All about proofs, Proofs for all, 55, 1 (2015), 23\u201344."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676982"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53518-6_5"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_23"},{"key":"e_1_2_2_7_1","volume-title":"Initial algebra semantics in matching logic","author":"Chen Xiaohong","unstructured":"Xiaohong Chen , Dorel Lucanu , and Grigore Ro\u015fu . 2020. Initial algebra semantics in matching logic . University of Illinois at Urbana-Champaign. http :\/\/hdl.handle.net\/2142\/107781 Xiaohong Chen, Dorel Lucanu, and Grigore Ro\u015fu. 2020. Initial algebra semantics in matching logic. University of Illinois at Urbana-Champaign. http:\/\/hdl.handle.net\/2142\/107781"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2021.100638"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785675"},{"key":"e_1_2_2_10_1","unstructured":"Xiaohong Chen and Grigore Ro\u015fu. 2019. Matching \u03bc -logic. University of Illinois at Urbana-Champaign. http:\/\/hdl.handle.net\/2142\/102281 \t\t\t\t  Xiaohong Chen and Grigore Ro\u015fu. 2019. Matching \u03bc -logic. University of Illinois at Urbana-Champaign. http:\/\/hdl.handle.net\/2142\/102281"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408970"},{"key":"e_1_2_2_12_1","unstructured":"Coq Team. 2021. Coq GitHub Repository. https:\/\/github.com\/coq\/coq \t\t\t\t  Coq Team. 2021. Coq GitHub Repository. https:\/\/github.com\/coq\/coq"},{"key":"e_1_2_2_13_1","unstructured":"Coq Team. 2021. The Coq proof assistant. http:\/\/coq.inria.fr \t\t\t\t  Coq Team. 2021. The Coq proof assistant. http:\/\/coq.inria.fr"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_29"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984027"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314601"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103719"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.336.2"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321997"},{"key":"e_1_2_2_22_1","volume-title":"A formal semantics of Python 3.3","author":"Guth Dwight","unstructured":"Dwight Guth . 2013. A formal semantics of Python 3.3 . University of Illinois at Urbana-Champaign. http :\/\/hdl.handle.net\/2142\/45275 Dwight Guth. 2013. A formal semantics of Python 3.3. University of Illinois at Urbana-Champaign. http:\/\/hdl.handle.net\/2142\/45275"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_24"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-26677-0"},{"key":"e_1_2_2_25_1","volume-title":"Standard ML. Department of Computer Science","author":"Harper Robert","unstructured":"Robert Harper , David MacQueen , and Robin Milner . 1986. Standard ML. Department of Computer Science , University of Edinburgh , Edinburgh, UK . http:\/\/www.lfcs.inf.ed.ac.uk\/reports\/86\/ECS-LFCS-86-2\/ Robert Harper, David MacQueen, and Robin Milner. 1986. Standard ML. Department of Computer Science, University of Edinburgh, Edinburgh, UK. http:\/\/www.lfcs.inf.ed.ac.uk\/reports\/86\/ECS-LFCS-86-2\/"},{"key":"e_1_2_2_26_1","volume-title":"Decision procedures for equationally based reasoning. Ph. D. Dissertation","author":"Hendrix Joseph D","unstructured":"Joseph D Hendrix . 2008. Decision procedures for equationally based reasoning. Ph. D. Dissertation . University of Illinois at Urbana-Champaign. http :\/\/hdl.handle.net\/2142\/11487 Joseph D Hendrix. 2008. Decision procedures for equationally based reasoning. Ph. D. Dissertation. University of Illinois at Urbana-Champaign. http:\/\/hdl.handle.net\/2142\/11487"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00022"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_29_1","unstructured":"Isabelle Team. 2021. Isabelle.  https:\/\/isabelle.in.tum.de\/ \t\t\t\t  Isabelle Team. 2021. Isabelle.  https:\/\/isabelle.in.tum.de\/"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_2_31_1","unstructured":"K Team. 2022. K framework Haskell backend. https:\/\/github.com\/kframework\/kore \t\t\t\t  K Team. 2022. K framework Haskell backend. https:\/\/github.com\/kframework\/kore"},{"key":"e_1_2_2_32_1","unstructured":"K Team. 2022. Matching logic proof checker. GitHub page. https:\/\/github.com\/kframework\/proof-generation See \t\t\t\t  K Team. 2022. Matching logic proof checker. GitHub page. https:\/\/github.com\/kframework\/proof-generation See"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446751"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535841"},{"key":"e_1_2_2_36_1","unstructured":"Xavier Leroy. 2020. The CompCert verified compiler software and commented proof. Available at. https:\/\/compcert.org\/ \t\t\t\t  Xavier Leroy. 2020. The CompCert verified compiler software and commented proof. Available at. https:\/\/compcert.org\/"},{"key":"e_1_2_2_37_1","volume-title":"Wheeler","author":"Levien Raph","year":"2019","unstructured":"Raph Levien and David A . Wheeler . 2019 . Metamath Verifier in Python . https:\/\/github.com\/david-a-wheeler\/mmverify.py Raph Levien and David A. Wheeler. 2019. Metamath Verifier in Python. https:\/\/github.com\/david-a-wheeler\/mmverify.py"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.7"},{"key":"e_1_2_2_39_1","unstructured":"Zhengyao Lin Xiaohong Chen Minh-Thai Trinh John Wang and Grigore Ro\u015fu. 2022. K Proof Generation Tool Repository. https:\/\/github.com\/kframework\/proof-generation \t\t\t\t  Zhengyao Lin Xiaohong Chen Minh-Thai Trinh John Wang and Grigore Ro\u015fu. 2022. K Proof Generation Tool Repository. https:\/\/github.com\/kframework\/proof-generation"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7503088"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_24"},{"key":"e_1_2_2_42_1","volume-title":"Wheeler","author":"Megill Norman","year":"2019","unstructured":"Norman Megill and David A . Wheeler . 2019 . Metamath : a computer language for mathematical proofs. Available at. http:\/\/us.metamath.org\/downloads\/metamath.pdf Norman Megill and David A. Wheeler. 2019. Metamath: a computer language for mathematical proofs. Available at. http:\/\/us.metamath.org\/downloads\/metamath.pdf"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/10721959_3"},{"key":"e_1_2_2_44_1","unstructured":"Stefan O\u2019Rear and Mario Carneiro. 2019. Metamath Verifier in Rust. https:\/\/github.com\/sorear\/smetamath-rs \t\t\t\t  Stefan O\u2019Rear and Mario Carneiro. 2019. Metamath Verifier in Rust. https:\/\/github.com\/sorear\/smetamath-rs"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737991"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_33"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(4:28)2017"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.42"},{"key":"e_1_2_2_51_1","volume-title":"Moore","author":"Ro\u015fu Grigore","year":"2012","unstructured":"Grigore Ro\u015fu , Andrei \u015etef\u0103nescu , \u015etefan Ciob\u00e2c\u0103 , and Brandon M . Moore . 2012 . Reachability Logic. University of Illinois at Urbana-Champaign. http:\/\/hdl.handle.net\/2142\/32952 Grigore Ro\u015fu, Andrei \u015etef\u0103nescu, \u015etefan Ciob\u00e2c\u0103, and Brandon M. Moore. 2012. Reachability Logic. University of Illinois at Urbana-Champaign. http:\/\/hdl.handle.net\/2142\/32952"},{"key":"e_1_2_2_52_1","volume-title":"Matching logic\u2014extended report","author":"Ro\u015fu Grigore","year":"2009","unstructured":"Grigore Ro\u015fu and Wolfram Schulte . 2009. Matching logic\u2014extended report . University of Illinois at Urbana-Champaign. https :\/\/fsl.cs.illinois.edu\/publications\/rosu-schulte- 2009 -tr.pdf Grigore Ro\u015fu and Wolfram Schulte. 2009. Matching logic\u2014extended report. University of Illinois at Urbana-Champaign. https:\/\/fsl.cs.illinois.edu\/publications\/rosu-schulte-2009-tr.pdf"},{"key":"e_1_2_2_53_1","volume-title":"Mathematical logic","author":"Shoenfield Joseph R.","unstructured":"Joseph R. Shoenfield . 1967. Mathematical logic . Addison-Wesley Pub . Co, Boston, United States. isbn:1-56881-135-7 Joseph R. Shoenfield. 1967. Mathematical logic. Addison-Wesley Pub. Co, Boston, United States. isbn:1-56881-135-7"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0163-3"},{"key":"e_1_2_2_56_1","unstructured":"SV-COMP. 2021. Benchmark for SV-COMP. https:\/\/gitlab.com\/sosy-lab\/benchmarking\/sv-benchmarks \t\t\t\t  SV-COMP. 2021. Benchmark for SV-COMP. https:\/\/gitlab.com\/sosy-lab\/benchmarking\/sv-benchmarks"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_2_58_1","unstructured":"Tukaani Team. 2021. XZ Utils. https:\/\/tukaani.org\/xz\/ \t\t\t\t  Tukaani Team. 2021. XZ Utils. https:\/\/tukaani.org\/xz\/"},{"key":"e_1_2_2_59_1","unstructured":"John Wang. 2022. Metamath proof checker in Rust. GitHub page. https:\/\/github.com\/kframework\/rust-metamath \t\t\t\t  John Wang. 2022. Metamath proof checker in Rust. GitHub page. https:\/\/github.com\/kframework\/rust-metamath"},{"key":"#cr-split#-e_1_2_2_60_1.1","unstructured":"Stefan Wils and Bart Jacobs. 2021. Certifying C program correctness with respect to CompCert with VeriFast. https:\/\/doi.org\/10.48550\/ARXIV.2110.11034 10.48550\/ARXIV.2110.11034"},{"key":"#cr-split#-e_1_2_2_60_1.2","unstructured":"Stefan Wils and Bart Jacobs. 2021. Certifying C program correctness with respect to CompCert with VeriFast. https:\/\/doi.org\/10.48550\/ARXIV.2110.11034"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586029","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3586029","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:10Z","timestamp":1750178770000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586029"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,6]]},"references-count":61,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2023,4,6]]}},"alternative-id":["10.1145\/3586029"],"URL":"https:\/\/doi.org\/10.1145\/3586029","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4,6]]},"assertion":[{"value":"2023-04-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}