DROPS

Artifact

Software

dafny-lang/b3

Authors: Vladimir Gladshtein and K. Rustan M. Leino

Abstract

Cite as

Vladimir Gladshtein, K. Rustan M. Leino. dafny-lang/b3 (Software, Dafny implementation). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-27039,
   title = {{dafny-lang/b3}}, 
   author = {Gladshtein, Vladimir and Leino, K. Rustan M.},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:1795668a148637332f93759bb96a4cd4283d6e32;origin=https://github.com/dafny-lang/b3;visit=swh:1:snp:648aaa9b8094ff8bbc35fddd2bcb5703151269fe;anchor=swh:1:rev:b24a2b2d6101df900e67d3bb151c4e85af4cd16d}{\texttt{swh:1:dir:1795668a148637332f93759bb96a4cd4283d6e32}} (visited on 2026-07-16)},
   url = {https://github.com/dafny-lang/b3},
   doi = {10.4230/artifacts.27039},
}

Document

DOI: 10.4230/LIPIcs.ITP.2026.6

Lazy Proof Automation for Separation Logic

Authors: Valentin Mikhalchuk, Vladimir Gladshtein, and Ilya Sergey

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract

Separation Logic is an established formalism for deductive verification of heap-manipulating programs. Proofs of symbolic heap entailment, an analogue of the ordinary logical implication, are amongst the most common reasoning steps in Separation Logic, and many existing heap verifiers provide automation for discharging valid heap entailments. We observe that existing techniques for automating entailment proofs in foundational Separation Logic verifiers embedded into provers such as Rocq, suffer from three main drawbacks: (a) poor performance due to metaprogramming overhead, (b) limited expressivity, and (c) restricted extensibility. To address these shortcomings, we propose lazy proof automation - an approach to entailment proofs inspired by translation validation. Our key idea is to implement an entailment checker as a combination of (1) an efficient but unverified prover, suitable for fast-paced interactive proofs, and (2) a proof reconstruction procedure that takes the prover’s trace and produces a certificate of entailment validity that can be checked a posteriori. We implemented these ideas in Yolo - a generic and extensible heap entailment prover built in Lean. We instantiate Yolo for two Lean-embedded Separation Logics and show its practical benefits, both in terms of user experience and proof-checking speed, compared with the automation available in state-of-the-art foundational Separation Logics.

Cite as

Valentin Mikhalchuk, Vladimir Gladshtein, and Ilya Sergey. Lazy Proof Automation for Separation Logic. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{mikhalchuk_et_al:LIPIcs.ITP.2026.6,
  author =	{Mikhalchuk, Valentin and Gladshtein, Vladimir and Sergey, Ilya},
  title =	{{Lazy Proof Automation for Separation Logic}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.6},
  URN =		{urn:nbn:de:0030-drops-269801},
  doi =		{10.4230/LIPIcs.ITP.2026.6},
  annote =	{Keywords: Lean, proof engineering, meta-programming}
}

Document

DOI: 10.4230/LIPIcs.ITP.2026.11

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

Authors: Vladimir Gladshtein and K. Rustan M. Leino

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{gladshtein_et_al:LIPIcs.ITP.2026.11,
  author =	{Gladshtein, Vladimir and Leino, K. Rustan M.},
  title =	{{Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.11},
  URN =		{urn:nbn:de:0030-drops-269855},
  doi =		{10.4230/LIPIcs.ITP.2026.11},
  annote =	{Keywords: Intermediate verification language, Soundness, Verification, B3, Dafny, SMT solvers}
}

Search Results

Documents authored by Gladshtein, Vladimir

dafny-lang/b3

Abstract

Cite as

Lazy Proof Automation for Separation Logic

Abstract

Cite as

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

Abstract

Cite as

Thanks for your feedback!

Could not send message