{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:54Z","timestamp":1780994634921,"version":"3.54.1"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001711","name":"Swiss National Science Foundation","doi-asserted-by":"crossref","award":["197065"],"award-info":[{"award-number":["197065"]}],"id":[{"id":"10.13039\/501100001711","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":[[2024,6,20]]},"abstract":"<jats:p>\n            Automated program verifiers are typically implemented using an intermediate verification language (IVL), such as Boogie or Why3. A verifier front-end translates the input program and specification into an IVL program, while the back-end generates proof obligations for the IVL program and employs an SMT solver to discharge them. Soundness of such verifiers therefore requires that the front-end translation faithfully captures the semantics of the input program and specification in the IVL program, and that the back-end reports success only if the IVL program is actually correct. For a verification tool to be trustworthy, these soundness conditions must be satisfied by its\n            <jats:italic toggle=\"yes\">actual implementation<\/jats:italic>\n            , not just the program logic it uses.\n          <\/jats:p>\n          <jats:p>In this paper, we present a novel validation methodology that, given a formal semantics for the input language and IVL, provides formal soundness guarantees for front-end implementations. For each run of the verifier, we automatically generate a proof in Isabelle showing that the correctness of the produced IVL program implies the correctness of the input program. This proof can be checked independently from the verifier, in Isabelle, and can be combined with existing work on validating back-ends to obtain an end-to-end soundness result. Our methodology based on forward simulation employs several modularisation strategies to handle the large semantic gap between the input language and the IVL, as well as the intricacies of practical, optimised translations. We present our methodology for the widely-used Viper and Boogie languages. Our evaluation shows that it is effective in validating the translations performed by the existing Viper implementation.<\/jats:p>","DOI":"10.1145\/3656438","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1510-1534","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1816-9256","authenticated-orcid":false,"given":"Gaurav","family":"Parthasarathy","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2719-4856","authenticated-orcid":false,"given":"Thibault","family":"Dardinier","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-9688-1299","authenticated-orcid":false,"given":"Benjamin","family":"Bonneau","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, Grenoble, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5554-9381","authenticated-orcid":false,"given":"Alexander J.","family":"Summers","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_3"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","unstructured":"Vytautas Astrauskas Peter M\u00fcller Federico Poli and Alexander J. Summers. 2019. Leveraging Rust Types for Modular Specification and Verification. Proc. ACM Program. Lang. 3 OOPSLA Article 147 30 pages. https:\/\/doi.org\/10.1145\/3360573 10.1145\/3360573","DOI":"10.1145\/3360573"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Michael Backes Catalin Hritcu and Thorsten Tarrach. 2011. Automatically Verifying Typing Constraints for a Data Processing Language. In Certified Programs and Proofs (CPP) Jean-Pierre Jouannaud and Zhong Shao (Eds.). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_22 10.1007\/978-3-642-25379-9_22","DOI":"10.1007\/978-3-642-25379-9_22"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","unstructured":"Stefan Blom Saeed Darabi Marieke Huisman and Wytse Oortwijn. 2017. The VerCors Tool Set: Verification of Parallel and Concurrent Software. In Integrated Formal Methods (IFM) Nadia Polikarpova and Steve Schneider (Eds.). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7 10.1007\/978-3-319-66845-1_7","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Sascha B\u00f6hme and Tjark Weber. 2010. Fast LCF-Style Proof Reconstruction for Z3. In Interactive Theorem Proving (ITP) Matt Kaufmann and Lawrence C. Paulson (Eds.). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_14 10.1007\/978-3-642-14052-5_14","DOI":"10.1007\/978-3-642-14052-5_14"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","unstructured":"John Boyland. 2003. Checking Interference with Fractional Permissions. In Static Analysis (SAS) Radhia Cousot (Ed.). 55\u201372. https:\/\/doi.org\/10.1007\/3-540-44898-5_4 10.1007\/3-540-44898-5_4","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","unstructured":"Montgomery Carter Shaobo He Jonathan Whitaker Zvonimir Rakamaric and Michael Emmi. 2016. SMACK software verification toolchain. In Proceedings of the 38th International Conference on Software Engineering ICSE 2016 Austin TX USA May 14-22 2016 \u2013 Companion Volume Laura K. Dillon Willem Visser and Laurie A. Williams (Eds.). ACM 589\u2013592. https:\/\/doi.org\/10.1145\/2889160.2889163 10.1145\/2889160.2889163","DOI":"10.1145\/2889160.2889163"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","unstructured":"David A. Cock Gerwin Klein and Thomas Sewell. 2008. Secure Microkernels State Monads and Scalable Refinement. In Theorem Proving in Higher Order Logics (TPHOLS) Otmane A\u00eft Mohamed C\u00e9sar A. Mu\u00f1oz and Sofi\u00e8ne Tahar (Eds.). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_16 10.1007\/978-3-540-71067-7_16","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632902"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Xavier Denis Jacques-Henri Jourdan and Claude March\u00e9. 2022. Creusot: A Foundry for the Deductive Verification of Rust Programs. In International Conference on Formal Engineering Methods (ICFEM) Adri\u00e1n Riesco and Min Zhang (Eds.) Vol. 13478. 90\u2013105. https:\/\/doi.org\/10.1007\/978-3-031-17244-1_6 10.1007\/978-3-031-17244-1_6","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_1_12_1","unstructured":"Boogie developers. 2022. Monomorphization of polymorphic maps and binders. https:\/\/github.com\/boogie-org\/boogie\/pull\/669 Accessed March 19 2024."},{"key":"e_1_3_1_13_1","unstructured":"Viper developers. 2024. Viper-to-Boogie implementation. https:\/\/github.com\/viperproject\/carbon Accessed April 4 2024."},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Jenna DiVincenzo Ian McCormack Hemant Gouni Jacob Gorenburg Mona Zhang Conrad Zimmerman Joshua Sunshine \u00c9ric Tanter and Jonathan Aldrich. 2022. Gradual C0: Symbolic Execution for Efficient Gradual Verification. CoRR abs\/2210.02428 (2022). https:\/\/doi.org\/10.48550\/ARXIV.2210.02428 10.48550\/ARXIV.2210.02428 arXiv:2210.02428","DOI":"10.48550\/ARXIV.2210.02428"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","unstructured":"Marco Eilers and Peter M\u00fcller. 2018. Nagini: A Static Verifier for Python. In Computer Aided Verification (CAV) Hana Chockler and Georg Weissenbacher (Eds.). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_33 10.1007\/978-3-319-96145-3_33","DOI":"10.1007\/978-3-319-96145-3_33"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","unstructured":"Marco Eilers Peter M\u00fcller and Samuel Hitz. 2018. Modular Product Programs. In European Symposium on Programming (ESOP) Amal Ahmed (Ed.). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_18 10.1007\/978-3-319-89884-1_18","DOI":"10.1007\/978-3-319-89884-1_18"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Burak Ekici Alain Mebsout Cesare Tinelli Chantal Keller Guy Katz Andrew Reynolds and Clark W. Barrett. 2017. SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. In Computer Aided Verification (CAV) Rupak Majumdar and Viktor Kuncak (Eds.). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_7 10.1007\/978-3-319-63390-9_7","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","unstructured":"Jean-Christophe Filli\u00e2tre and Andrei Paskevich. 2013. Why3 \u2014 Where Programs Meet Provers. In European Symposium on Programming (ESOP) Matthias Felleisen and Philippa Gardner (Eds.). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8 10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","unstructured":"Mathias Fleury and Hans-J\u00f6rg Schurr. 2019. Reconstructing veriT Proofs in Isabelle\/HOL. In Workshop on Proof eXchange for Theorem Proving (PxTP) Giselle Reis and Haniel Barbosa (Eds.). https:\/\/doi.org\/10.4204\/EPTCS.301.6 10.4204\/EPTCS.301.6","DOI":"10.4204\/EPTCS.301.6"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","unstructured":"Quentin Garchery. 2021. A Framework for Proof-carrying Logical Transformations. In Workshop on Proof eXchange for Theorem Proving (PxTP) Chantal Keller and Mathias Fleury (Eds.). https:\/\/doi.org\/10.4204\/EPTCS.336.2 10.4204\/EPTCS.336.2","DOI":"10.4204\/EPTCS.336.2"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"L\u00e9o Gourdin Benjamin Bonneau Sylvain Boulm\u00e9 David Monniaux and Alexandre B\u00e9rard. 2023. Formally Verifying Optimizations with Block Simulations. Proc. ACM Program. Lang. 7 OOPSLA2 Article 224 (oct 2023) 30 pages. https:\/\/doi.org\/10.1145\/3622799 10.1145\/3622799","DOI":"10.1145\/3622799"},{"key":"e_1_3_1_22_1","volume-title":"Certification of a Tool Chain for Deductive Program Verification. (Certification d\u2019une chaine de v\u00e9rification d\u00e9ductive de programmes)","author":"Herms Paolo","year":"2013","unstructured":"Paolo Herms. 2013. Certification of a Tool Chain for Deductive Program Verification. (Certification d\u2019une chaine de v\u00e9rification d\u00e9ductive de programmes). Ph.D. Dissertation. University of Paris-Sud, Orsay, France. https:\/\/tel.archives-ouvertes.fr\/tel-00789543"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","unstructured":"Ioannis T. Kassios. 2006. Dynamic Frames: Support for Framing Dependencies and Sharing Without Restrictions. In Formal Methods (FM) Jayadev Misra Tobias Nipkow and Emil Sekerinski (Eds.). https:\/\/doi.org\/10.1007\/11813040_19 10.1007\/11813040_19","DOI":"10.1007\/11813040_19"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-1539-9_11"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635894"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.059"},{"key":"e_1_3_1_29_1","unstructured":"K. Rustan M. Leino. 2008. This is Boogie 2. (2008). Available from http:\/\/research.microsoft.com\/en-us\/um\/people\/leino\/papers\/krml178.pdf."},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming Artificial Intelligence and Reasoning (LPAR) Edmund M. Clarke and Andrei Voronkov (Eds.). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20 10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","unstructured":"K. Rustan M. Leino and Philipp R\u00fcmmer. 2010. A Polymorphic Intermediate Verification Language: Design and Logical Encoding. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) Javier Esparza and Rupak Majumdar (Eds.). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_26 10.1007\/978-3-642-12002-2_26","DOI":"10.1007\/978-3-642-12002-2_26"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586029"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_3_1_34_1","unstructured":"Claude March\u00e9 and Yannick Moy. 2018. The Jessie plugin for Deductive Verification in Frama-C. http:\/\/krakatoa.lri.fr\/jessie.pdf"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","unstructured":"Peter M\u00fcller Malte Schwerhoff and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Verification Model Checking and Abstract Interpretation (VMCAI) Barbara Jobstmann and K. Rustan M. Leino (Eds.). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2 10.1007\/978-3-662-49122-5_2","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(3:1)2012"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","unstructured":"Gaurav Parthasarathy Thibault Dardinier Benjamin Bonneau Peter M\u00fcller and Alexander J. Summers. 2024. Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language \u2013 Artifact. https:\/\/doi.org\/10.5281\/zenodo.10802176 10.5281\/zenodo.10802176","DOI":"10.5281\/zenodo.10802176"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","unstructured":"Gaurav Parthasarathy Thibault Dardinier Benjamin Bonneau Peter M\u00fcller and Alexander J. Summers. 2024. Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version). https:\/\/doi.org\/10.48550\/ARXIV.2404.03614 10.48550\/ARXIV.2404.03614 arXiv:2404.03614 [cs.PL]","DOI":"10.48550\/ARXIV.2404.03614"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","unstructured":"Gaurav Parthasarathy Peter M\u00fcller and Alexander J. Summers. 2021. Formally Validating a Practical Verification Condition Generator. In Computer Aided Verification (CAV) (LNCS Vol. 12760) Alexandra Silva and K. Rustan M. Leino (Eds.). 704\u2013727. https:\/\/doi.org\/10.1007\/978-3-030-81688-9_33 10.1007\/978-3-030-81688-9_33","DOI":"10.1007\/978-3-030-81688-9_33"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","unstructured":"Christine Rizkallah Japheth Lim Yutaka Nagashima Thomas Sewell Zilin Chen Liam O\u2019Connor Toby C. Murray Gabriele Keller and Gerwin Klein. 2016. A Framework for the Automatic Formal Verification of Refinement from Cogent to C.. In Interactive Theorem Proving (ITP) Jasmin Christian Blanchette and Stephan Merz (Eds.). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_20 10.1007\/978-3-319-43144-4_20","DOI":"10.1007\/978-3-319-43144-4_20"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160911"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","unstructured":"Jean-Baptiste Tristan and Xavier Leroy. 2008. Formal verification of translation validators: a case study on instruction scheduling optimizations. In Principles of Programming Languages (POPL) George C. Necula and Philip Wadler (Eds.). https:\/\/doi.org\/10.1145\/1328438.1328444 10.1145\/1328438.1328444","DOI":"10.1145\/1328438.1328444"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","unstructured":"Jean-Baptiste Tristan and Xavier Leroy. 2009. Verified validation of lazy code motion. In Programming Language Design and Implementation (PLDI) Michael Hind and Amer Diwan (Eds.). https:\/\/doi.org\/10.1145\/1542476.1542512 10.1145\/1542476.1542512","DOI":"10.1145\/1542476.1542512"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-95891-8_51"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2308.15567"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","unstructured":"Simon Winwood Gerwin Klein Thomas Sewell June Andronick David A. Cock and Michael Norrish. 2009. Mind the Gap. In Theorem Proving in Higher Order Logics (TPHOLS) Stefan Berghofer Tobias Nipkow Christian Urban and Makarius Wenzel (Eds.). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_34 10.1007\/978-3-642-03359-9_34","DOI":"10.1007\/978-3-642-03359-9_34"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","unstructured":"Felix A. Wolf Linard Arquint Martin Clochard Wytse Oortwijn Jo\u00e3o Carlos Pereira and Peter M\u00fcller. 2021. Gobra: Modular Specification and Verification of Go Programs. In Computer Aided Verification (CAV) Alexandra Silva and K. Rustan M. Leino (Eds.). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_17 10.1007\/978-3-030-81685-8_17","DOI":"10.1007\/978-3-030-81685-8_17"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632927"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656438","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656438","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:38:51Z","timestamp":1751661531000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656438"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":48,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656438"],"URL":"https:\/\/doi.org\/10.1145\/3656438","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}