Document Open Access Logo

Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language

Authors Vladimir Gladshtein , K. Rustan M. Leino

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.11.pdf
  • Filesize: 0.85 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification and validation
Keywords
  • Intermediate verification language
  • Soundness
  • Verification
  • B3
  • Dafny
  • SMT solvers

Metrics

Abstract

Intermediate Verification Languages (IVLs) play the same role in verification as Intermediate Representations in compilation, a layer that separates a verifier’s language-specific front-end from its logic automation back-end. Successful IVL tools such as Boogie, Why3, and Viper generate Verification Conditions (VCs) that are sent to an SMT solver. The verifier output can be trusted only if these VCs are sound with respect to the formal semantics of the IVL. Formalizing the semantics of IVLs and verifying the soundness of corresponding VC Generators with respect to this semantics is challenging if one wants to model realistic features of IVLs such as mutually recursive definitions, lexical variable and control-flow labeled scopes, interpreted and uninterpreted functions, and unbounded loops.
B3 is a new IVL. This paper presents a formalization of B3’s semantics, a VC Generator for the language, and a soundness proof that these two correspond. A key practical contribution of this work is that all three components are authored in the Dafny programming language and verifier. This makes it easy for a tool maintainer to maneuver between the semantic definitions, the proofs, and the VCG’s executable code. The key theoretical contribution of the work is a methodology to split the IVL’s semantic encodings into two layers of abstraction to cover realistic aspects of the semantics, while keeping the proofs amenable to automation. Optimized for Dafny-style automation, the first layer is used to verify the correctness of the VC Generator procedure. Optimized for expressiveness, the second layer is used to capture the semantics in a natural way.

Cite As Get BibTex

Vladimir Gladshtein and K. Rustan M. Leino. Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.11

Author Details

Vladimir Gladshtein
  • National University of Singapore, Singapore
K. Rustan M. Leino
  • Amazon Web Services, Seattle, WA, USA

Funding

  • Gladshtein, Vladimir: Work done during an internship at Amazon Web Services.

Supplementary Materials

References

  1. Anysphere. Cursor: The AI code editor. https://cursor.com, 2026. Accessed: 2026-05-04.
  2. Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever, editors, Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, volume 4111 of Lecture Notes in Computer Science, pages 364-387. Springer, 2005. URL: https://doi.org/10.1007/11804192_17.
  3. Arthur Charguéraud, Adam Chlipala, Andres Erbsen, and Samuel Gruetter. Omnisemantics: Smooth handling of nondeterminism. ACM Trans. Program. Lang. Syst., 45(1), 2023. URL: https://doi.org/10.1145/3579834.
  4. Joshua M. Cohen and Philip Johnson-Freyd. A formalization of core Why3 in Coq. Proc. ACM Program. Lang., 8(POPL), January 2024. URL: https://doi.org/10.1145/3632902.
  5. Flaviu Cristian. Correct and robust programs. IEEE Trans. Software Eng., 10(2):163-174, 1984. URL: https://doi.org/10.1109/TSE.1984.5010218.
  6. Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, and Peter Müller. Formal foundations for translational separation logic verifiers. Proc. ACM Program. Lang., 9(POPL), January 2025. URL: https://doi.org/10.1145/3704856.
  7. Edsger W. Dijkstra. A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ, 1976. Google Scholar
  8. Marco Eilers, Malte Schwerhoff, and Peter Müller. Verification algorithms for automated separation logic verifiers. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pages 362-386. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_18.
  9. Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - Where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, Proceedings of the 22nd European Symposium on Programming, volume 7792 of Lecture Notes in Computer Science, pages 125-128. Springer, March 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_8.
  10. Cormac Flanagan and James B. Saxe. Avoiding exponential explosion: generating compact verification conditions. In Chris Hankin and Dave Schmidt, editors, Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 193-205. Association for Computing Machinery, 2001. URL: https://doi.org/10.1145/360204.360220.
  11. Vladimir Gladshtein and K. Rustan M. Leino. dafny-lang/b3. Software, (visited on 2026-07-08). URL: https://github.com/dafny-lang/b3
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.27039
  12. John Harrison, Josef Urban, and Freek Wiedijk. History of interactive theorem proving. In Jörg H. Siekmann, editor, Computational Logic, volume 9 of Handbook of the History of Logic, pages 135-214. Elsevier, 2014. URL: https://doi.org/10.1016/B978-0-444-51624-4.50004-6.
  13. P. V. Homeier and D. F. Martin. A mechanically verified verification condition generator. The Computer Journal, 38(2):131-141, January 1995. URL: https://doi.org/10.1093/comjnl/38.2.131.
  14. James C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385-394, July 1976. URL: https://doi.org/10.1145/360248.360252.
  15. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 179-191. Association for Computing Machinery, 2014. URL: https://doi.org/10.1145/2535838.2535841.
  16. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Edmund M. Clarke and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, volume 6355 of Lecture Notes in Computer Science, pages 348-370. Springer, April 2010. URL: https://doi.org/10.1007/978-3-642-17511-4_20.
  17. K. Rustan M. Leino. Automating induction with an SMT solver. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, volume 7148 of Lecture Notes in Computer Science, pages 315-331. Springer, January 2012. URL: https://doi.org/10.1007/978-3-642-27940-9_21.
  18. K. Rustan M. Leino. Automating theorem proving with SMT. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving - 4th International Conference, ITP 2013, volume 7998 of Lecture Notes in Computer Science, pages 2-16. Springer, July 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_2.
  19. K. Rustan M. Leino. Well-founded functions and extreme predicates in Dafny: A tutorial. In Boris Konev, Stephan Schulz, and Laurent Simon, editors, IWIL-2015. 11th International Workshop on the Implementation of Logics, volume 40 of EPiC Series in Computing, pages 52-66. EasyChair, 2016. URL: https://doi.org/10.29007/v2m3.
  20. K. Rustan M. Leino and Michał Moskal. Co-induction simply - automatic co-inductive proofs in a program verifier. In Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: Formal Methods - 19th International Symposium, volume 8442 of Lecture Notes in Computer Science, pages 382-398. Springer, May 2014. URL: https://doi.org/10.1007/978-3-319-06410-9_27.
  21. Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107-115, 2009. URL: https://doi.org/10.1145/1538788.1538814.
  22. Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A verification infrastructure for permission-based reasoning. In Barbara Jobstmann and K. Rustan M. Leino, editors, Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, volume 9583 of Lecture Notes in Computer Science, pages 41-62. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49122-5_2.
  23. Daniel Nezamabadi, Magnus O. Myreen, and Yong Kiam Tan. Verified VCG and verified compiler for Dafny. In CPP 2026, 2026. URL: https://api.semanticscholar.org/CorpusID:283672227.
  24. David Lorge Parnas. A technique for software module specification with examples. Commun. ACM, 15(5):330-336, 1972. URL: https://doi.org/10.1145/355602.361309.
  25. Gaurav Parthasarathy, Peter Müller, and Alexander J. Summers. Formally validating a practical verification condition generator. In Computer Aided Verification: 33rd International Conference, CAV 2021, Proceedings, Part II, pages 704-727, Berlin, Heidelberg, 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-81688-9_33.
  26. Frédéric Vogels, Bart Jacobs, and Frank Piessens. Featherweight VeriFast. Logical Methods in Computer Science, 11(3), 2015. URL: https://doi.org/10.2168/LMCS-11(3:19)2015.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact