Pith. sign in

REVIEW 3 major objections 4 minor 34 references

Gradually Verifying Unfolding Expressions & Pure Functions

T0 review · 3 major / 4 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Gradual verification of unfolding expressions and pure functions is sound: accepted programs always pass the generated runtime checks.

desk verdict Useful formalization of a real gap, but the soundness proof relies on a mutual induction whose well-foundedness is never demonstrated. read the letter →

arxiv 2607.15383 v1 pith:PYGMZDHG submitted 2026-07-16 cs.PL

Hazel Torek , Long Tien Nguyen , Priyam Gupta , Jenna DiVincenzo , Jonathan Aldrich This is my paper · ORCID
classification cs.PL MSC 68Q6003B70
keywords gradualverificationsymbolicexecutionunfoldingexpressionspurefunctionsimplicitdynamicframessoundnessproofruntimechecksViper
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Unfolding expressions and pure functions are the workhorse constructs that make ownership-based specifications modular—unfolding temporarily opens a predicate to reach the fields it owns, and pure functions let specifications call recursive heap-dependent functions—yet neither had a formal semantics or soundness proof for symbolic-execution verifiers. This paper supplies both for a static verifier and extends them to a gradual verifier, where imprecise specifications create optimistic assumptions that are backed by runtime checks. The central result is a soundness theorem for the new rules: whenever the verifier accepts a program, the run-time checks it generates will all succeed during execution, so there is no false acceptance. Because the gradual verifier is a conservative extension of the static one, the result transfers to the static symbolic-execution backend underlying several Viper-based tools. If correct, this closes a foundational gap for modular verification and makes gradual verification a viable route for real codebases that already rely on these constructs.

What carries the argument

The symbolic state σ = ⟨ι, H, H, γ, g, V⟩—imprecision flag, precise heap, optimistic heap, store, path condition, and a visited set of already-unfolded predicates/functions—along with the evaluation rules SEvalUnfolding* and SEvalFunction* that consume a predicate/precondition, produce its body, evaluate the inner expression under the temporary permissions, then restore the state. The visited-set recursion cutoff replaces recursive evaluations with fresh uninterpreted values, and the symbolic footprint J·Kσ computes the heap snapshot needed to evaluate pure-function bodies and postconditions. Soundness is carried by corresponding valuations that map symbolic values to the concrete values of

What would settle it

Run a verified program that uses a recursive pure function with an imprecise precondition and an inner expression that reads a field optimistically assumed during a recursive call—for instance, the paper's sum example with 'requires ?' and body 'node != null ? node.val + sum(node.next) : 0'—and execute the client. If the generated run-time checks omit a needed field or any check fails on a program the verifier accepted, the soundness theorem is false. A second check: mechanically verify the mutual induction over Expr ∪ Formula and see whether a decreasing measure can actually be constructed.

Watch

Extended reading notes

Core claim

The paper's claim, on its own terms, is that the symbolic-evaluation rules for unfolding expressions and pure-function applications—Figures 4, 6, 8, 11 through 13—together with the extended dynamic semantics and correspondence, are sound. Concretely, Theorems 1–3 establish progress and preservation: a valid dynamic state can always take a step when the matching run-time checks are satisfied, and every step preserves validity. The proof introduces the machinery that makes this hold: a visited set cuts unbounded recursion by replacing recursive unfolding/function evaluation with an uninterpreted fresh value (while still checking the predicate/precondition exists), a symbolic footprint snapshot

Load-bearing premise

The proof stands on a well-founded mutual induction over expressions and formulas—a size measure that the paper asserts but never defines—and on the recursion-cut rules' fresh uninterpreted values faithfully representing the full runtime result of the skipped evaluation.

Editorial extensions

If this is right

  • Accepted programs can no longer fail their own checks: the generated run-time checks are guaranteed to hold on every execution of a verified program.
  • Static symbolic-execution verifiers built on the same backend inherit the soundness result, since gradual verification reduces to static verification on fully-specified programs.
  • Developers can use unfolding expressions and recursive pure functions in specifications without worrying about unsoundness from recursion cutoffs—the cutoff is incomplete but never unsound.
  • Imprecise specifications with '?' can now cover heap-dependent expressions, with the verifier generating runtime checks for optimistically assumed fields and predicate instances.
  • The semantics pin down when optimistic assumptions survive an unfolding: retained for imprecise initial states, discarded for imprecise predicate bodies—a distinction that future verifier implementations can rely on.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The mutual recursion between expression and formula semantics in the soundness proof suggests that any future construct mixing the two—quantified permissions, fractional permissions—will need the same coupled induction; the paper's structure provides a template.
  • The proof's asserted-but-unstated size measure for the mutual induction invites mechanization; formalizing this proof in a proof assistant would either produce the missing measure or expose a gap.
  • A concrete testable prediction: in recursive-pure-function-heavy verified code, the recursion-cut incompleteness should rarely surface; measuring how often manual unfolding is needed could quantify the practical cost.
  • The visited set could be replaced by a multiset to allow a configurable recursion cutoff depth, which the paper notes; this suggests an easy experimental knob for balancing completeness and termination.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper formalizes symbolic-execution semantics for unfolding expressions and pure functions in Viper-style implicit-dynamic-frames verifiers, extends these semantics to the gradual verifier Gradual C0/Gradual Viper with imprecise specifications and run-time checks, and claims a soundness proof for the resulting system. The static and gradual inference rules (Figures 4, 6, 8, 11), the dynamic evaluation/framing rules (Figures 12–13), and the state-correspondence machinery are presented in detail, with a large appendix containing the lemmas and theorems that are supposed to establish progress and preservation. The central claim is that, if these rules are correct, a program that passes static verification will only fail at run time when a generated run-time check fails.

Significance. The target constructs are widely used in Viper-based verifiers (Gobra, Nagini, SnaKt), and the paper addresses a real gap: prior formalizations of Viper and Gradual C0 do not cover unfolding expressions or pure functions. If the soundness result is established, it would also transfer to static symbolic-execution backends by conservative extension, which would be a useful contribution to the verification community. The paper gives a careful, example-driven account of several delicate design choices (visited sets for recursion cutoff, heap snapshots via symbolic footprints, optimistic heaps and run-time checks, correspondence between symbolic and dynamic states), and it is honest about its limitations. However, the proof of soundness is hand-written, explicitly not mechanized, and contains an unresolved mutual-induction step that is load-bearing for the main theorem. The paper is therefore best regarded as a substantial formalization effort and proof sketch that needs completion before the soundness claim can be accepted.

major comments (3)
  1. [Section 4 / Appendix D, Lemma 26 vs. Lemma 41] The soundness proof has a genuine circularity that is acknowledged but not resolved. Lemma 26 (Soundness of evaluation) is proved by induction on the evaluation derivation, but its Cases 13 and 17 invoke Lemma 43 (Soundness of consume); Lemma 43 is derived from Lemma 41, whose proof cases (SConsumeValue, SConsumePredicate, SConsumeAcc) invoke Lemma 26 to evaluate argument expressions. Section 4 asserts that this can be handled by induction on the size of the term and by mutual induction, but no concrete size measure is supplied. This is not cosmetic: the footprint definitions in Appendix B.4 and C.3 substitute predicate and function bodies, which need not be syntactic subterms and can be larger than the original instance, and the evaluation rules for unfolding and pure functions consume formulae that are not subexpressions of the original expression. Please provide an explicit well-found
  2. [Appendix D, first paragraph (inherited lemmas)] The text says that lemmas stated without proof 'have the same proof as Zimmerman et al.' This is not enough in the new dependency graph. The prior proof had a one-directional dependency of consume lemmas on the evaluation lemma; the new Lemma 26 has cases that call consume lemmas, so Lemma 41 now depends on Lemma 26 for the very cases that were previously independent. Key lemmas such as 42 and 43 are not proved in this manuscript, and their previous proofs cannot be assumed to carry over unchanged. Since the central claim is soundness, the authors should either prove the adapted lemmas in the new setting or provide a machine-checked proof artifact that makes the dependency graph explicit and verifiable.
  3. [Appendix C.6, axiomatize definition; Appendix A grammar] The grammar permits pure-function applications inside expressions, hence inside function postconditions (func_post), but the axiomatize function is defined only for literals, variables, field accesses, binary/logical operators, and unfolding expressions. There is no case for a pure-function call, including nested calls. Consequently, SEvalFunctionExplicit and SEvalFunctionImplicit are under-defined for a function whose postcondition contains another pure-function application. This is a load-bearing incompleteness in the formal semantics, not a presentation issue. Either extend axiomatize with a recursive case for pure-function calls and prove a matching soundness property, or explicitly restrict the grammar/well-formedness conditions to exclude such postconditions.
minor comments (4)
  1. [Theorem 2 statement] The last sentence says 'where V′ is the corresponding valuation extending V′'; this should presumably be 'extending V'. Please correct the typo.
  2. [References [32] and [33]] References [32] and [33] appear to be the same paper by the same authors with the same title and year, cited with different publication details. This is confusing; please consolidate into a single reference or explicitly explain why two entries are needed.
  3. [Appendix B.4, footprint notation] The notation T𝑒U⟨𝐻,𝜌⟩ ;⟨ℓ, 𝑓⟩ in the exact-footprint clauses is unclear; it appears to mean union with the singleton {⟨ℓ,𝑓⟩}. Please define the intended operation explicitly.
  4. [Definition 3 / Figures 8 and 11] The static rules in Figures 8 and 11 branch on whether a predicate or function body is 'precise'/'imprecise'. Definition 3 defines 'completely precise' for formulas, but it would help to state explicitly how this is decided statically for a predicate body, especially when predicate bodies refer to other predicates, and to confirm that 'imprecise' means 'not completely precise'.

Circularity Check

2 steps flagged · score 4.0 of 10

Mutual dependence of evaluation- and consume-soundness lemmas lacks an explicit well-founded order, and recursion-cut correspondence is fixed to the run-time result by Definition 36.

  1. self definitional [Appendix D.2 (Definition 36); Lemma 26, Cases 14 and 18]
    "SEvalUnfoldingImplicitPrecise or SEvalUnfoldingImplicitImprecise: V[σ1⊢unfolding p(e) in e0⇓t⊣σ2,R|H,ρ] := V[σ1⊢e⇓t⊣σ2,R|H,ρ][t↦→v] where ⟨H,ρ⟩⊢e0⇓v. ... Case 14: 'By Definition 36, ⟨H,ρ⟩⊢e0⇓V′(t), so therefore ⟨H,ρ⟩⊢unfolding p(e) in e0⇓V′(t).'"

    For the recursion-cut rules the symbolic result is a fresh uninterpreted constant; Definition 36 fixes the corresponding valuation by first running the inner expression/body at run time. The soundness theorem's evaluation conclusion for this case is therefore the definition of V′, not a consequence of the static derivation or checks. The same holds for SEvalFunctionImplicit, where f(t,s) is mapped to the runtime value of func_body(f). So the claimed 'soundness' for these branches is partially by construction.

  2. other [§4 Soundness; Appendix D.2 Lemma 26 vs Appendix D.4 Lemma 41/43]
    "Conceptually, this theorem can be proved by induction on the size of the term. Our formalization uses this intuition but concretely realizes it via mutual induction over the previous decoupled theorems. ... Lemma 26 Case 13: 'Then, by Lemma 43, ⟨H,α,ρ⟩⊨p(e) and ⟨H,α\Tp(e)U⟨H,ρ⟩,ρ⟩ V′ σ3 ...' ... Lemma 41 Case 5: 'Therefore, for each e and corresponding t, ⟨H,ρ⟩⊢e⇓V′(t) by lemma 26.'"

    Lemma 26 (evaluation soundness) is proved by induction on evaluation derivations but its unfolding/function cases apply Lemma 43 (consume soundness). Lemma 41/43 is proved for consume derivations and its predicate/accessibility cases call Lemma 26 to evaluate argument expressions. The paper acknowledges the mutual dependence but gives no concrete well-founded measure; the suggested 'size of the term' is not obviously decreasing because predicate and function bodies are substituted and can grow. As written, the two lemma families prove each other without a demonstrated base/ordering, leaving a circular core in the soundness proof.

full rationale

Most circularity patterns do not apply: there is no fitted parameter being relabeled as a prediction, no imported uniqueness theorem, and no hidden ansatz passed through a citation; the semantics are presented as explicit inference rules. The reliance on Zimmerman et al. is same-group self-citation, but it is prior published work and by itself would not be circular. However, the appendix delegates many unproved lemmas to that prior paper ('lemmas and theorems stated without proof have the same proof as Zimmerman et al.'), so a substantial part of the proof rests on a self-citation chain, though not uniquely so. The main circularity concern is the unmeasured mutual recursion between Lemma 26 and Lemma 41/43: evaluation soundness for unfolding/pure-function cases appeals to consume soundness, while consume soundness appeals to evaluation soundness for argument and body evaluation. The paper explicitly notes that expression lemmas and formula lemmas now depend on each other and asserts an induction on term size without supplying the measure; since substitution into predicate/function bodies can increase term size, the stated remedy is not demonstrated. A second, narrower by-construction issue is Definition 36, which maps fresh recursion-cut symbols to the already-known runtime results, making part of the soundness theorem's evaluation clause true by definition rather than by static derivation. These issues are localized to the recursive and consume-based cases; the explicit evaluation rules, framing lemmas, and run-time check generation still have substantial independent content. Overall this is partial circularity/incompleteness rather than a fully forced derivation, so a score of 4 is appropriate.

Assumptions & free parameters 3 free parameters · 6 assumptions · 3 invented entities

The central claim depends on: (1) the inherited soundness of the Zimmerman et al. base proof; (2) the asserted conservative-extension transfer to static Silicon; (3) the asserted well-founded mutual induction over Expr ∪ Formula; (4) the correspondence of recursion-cut fresh values to full runtime results; and (5) program well-formedness conditions. No numeric parameters are fitted to data; the free parameters listed are hand-chosen design constants of the formalization (recursion depth, optimistic-heap retention, full-heap capture) that the soundness argument's shape depends on. The invented entities are formal mechanisms (symbolic footprint, axiomatize, optimistic predicate chunks) with no independent external evidence; they are validated only by the paper's own proof, which is the claim under review.

free parameters (3)
  • Recursion cutoff depth for the visited set V
    Design constant: V is a plain set, so recursive unfolding/function application is cut after depth 1 (§2.3: 'it could easily be exchanged for a multiset to enable a specified cutoff depth rather than only allowing a depth of one'). The soundness of all implicit rules (Figs. 4, 6, 8, 11) depends on this depth choice.
  • Optimistic-heap retention policy in SEvalUnfoldingImpreciseA/B
    Hand-chosen policy: whether optimistic assumptions accumulated during the inner expression are retained in the final optimistic heap depends on whether the predicate body is precise (Fig. 8; §3.2). This determines which run-time checks are generated and is a design decision, not a forced derivation.
  • Full-heap capture for imprecise symbolic footprints
    §3.3: J?*phi K_sigma = H(sigma) ∪ H(sigma) — the symbolic footprint of an imprecise specification captures the entire heap, including unrelated chunks (e.g., the t_z.val chunk in Fig. 9's example). This conservative choice directly affects the size of run-time check sets R3 for recursive calls.
assumptions (6)
  • domain assumption Program well-formedness (Definition 1): function bodies and post-conditions are framed by pre-conditions; imprecise pre-condition forces imprecise post-condition; function post-conditions evaluate in the produced precondition state.
    Stated in Appendix A, Definition 1, and used throughout the framing lemmas (Lemma 1 Case 9: 'By Definition 1, this implies ... framed'). If a verifier admitted a function whose body is not framed by its precondition, the evaluation soundness argument (Lemma 26 Case 17) collapses.
  • domain assumption Soundness of the base system: Zimmerman et al. [32]'s Gradual Viper formalization is correct, and the new proof inherits all unstated lemmas from it.
    Appendix D: 'Lemmas 1 to 27 in our proof have the same numbering as in the proof of soundness in [33]... lemmas and theorems stated without proof have the same proof as Zimmerman et al.' The chain is not mechanized (paper §6 admits no proof assistant was used).
  • domain assumption Gradual verification is a conservative extension of static verification, so soundness of the gradual system transfers to the static Viper/Silicon backend.
    Abstract and §1: 'because the gradual verifier is a conservative extension of a static verifier, our results also apply to static verifiers that use symbolic execution, such as the Silicon symbolic execution backend.' This property is imported from [29,32]; no conservativity lemma restricting the new gradual rules to precise states and matching Silicon's actual rules is proven.
  • domain assumption SMT solver soundness: path-condition satisfiability checks provided to the underlying SMT solver are correct.
    §2.4: 'the Zimmerman et al. formalization does not directly interface with the underlying SMT solver beyond implicitly assuming its soundness.' The paper states it deliberately avoids SMT-level axioms (unlike Silicon's quantifier-triggering approach) because of this assumption.
  • ad hoc to paper Well-founded mutual induction over Expr ∪ Formula with a size measure compatible with the non-structural footprint definitions.
    §4: the framing monotonicity theorems for expressions and formulas 'rely on each other' and the resolution is asserted: 'this theorem can be proved by induction on the size of the term. Our formalization uses this intuition but concretely realizes it via mutual induction.' The concrete measure is never given, and Appendix B.4 defines T p(e) U via substitution into the (potentially larger) predicate body, and J·Kσ is defined through evaluation — both non-structurally recursive.
  • ad hoc to paper Correspondence for recursion-cut rules: an uninterpreted fresh symbolic value can be mapped by the corresponding valuation to the full runtime evaluation result without violating path-condition consistency.
    Definition 36 maps the fresh value from SEvalUnfoldingImplicit* to v where ⟨H, rho⟩ ⊢ e0 ⇓ v, and SEvalFunctionImplicit to the body's runtime value; Lemma 26 cases 14-16 and 18 rely on this. The soundness of this substitution under later path-condition constraints is the structurally weakest point of the proof, and the paper flags only its incompleteness, not this dependency.
invented entities (3)
  • Symbolic footprint J·K_sigma of a formula
    purpose: Computes the heap snapshot implicitly passed to pure function applications during symbolic evaluation (SEvalFunctionExplicit/Implicit).
    Introduced in §2.4 and Appendix C.3. It is defined mutually-recursively with symbolic evaluation (J e.f K_sigma requires sigma ⊢ e ⇓ t_e and sigma ⊢ t_e.f ⇓ t), so its well-definedness is an internal design assumption; it has no external falsifiable handle.
  • axiomatize function
    purpose: Lifts a pure function's post-condition expression into path-condition constraints over the fresh function symbol f(t,s) and the heap snapshot.
    New helper defined in §2.4 and C.6. Its rule for unfolding expressions inside post-conditions is to discard the unfolding (axiomatize(...)(unfolding p(e) in e0) = axiomatize(...)(e0)), and it substitutes field accesses from the snapshot; the adequacy of this treatment is part of the paper's design, not an externally verified fact.
  • Predicate chunks in the optimistic heap
    purpose: Allows optimistic ownership of predicate instances ⟨p,t⟩ in imprecise states so unfolding can succeed statically and be re-checked at runtime.
    Extension of Zimmerman et al.'s optimistic heap (which held only field chunks) to hold predicate chunks, §3.1.1 and Appendix C.4 (equation 2). The correspondence now requires each optimistic predicate instance to hold in the dynamic state; Lemma 26 cases 14-15 depend on this extension.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Gradually Verifying Unfolding Expressions & Pure Functions." pith.science (2026). https://pith.science/paper/PYGMZDHG

@misc{pith2026260715383,
  author       = {Pith},
  title        = {Pith review of: Gradually Verifying Unfolding Expressions & Pure Functions},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PYGMZDHG}},
  note         = {Machine review of arXiv:2607.15383}
}
read the original abstract

Unfolding expressions, which temporarily unfold a predicate to leverage its owned fields when evaluating a heap-dependent expression, and pure functions, which are heap-dependent functions that can be used in specifications, are used in deductive program verifiers based on implicit dynamic frames, such as Gradual C0, Gobra, Nagini, and SnaKt, to increase the modularity of specifications involving ownership. In this paper, we present the formal semantics for unfolding expressions and pure functions for a static verifier using symbolic execution, extend it for a gradual verifier, and provide a proof of soundness. To support Gradual C0, our proof is in the setting of gradual verification, a deductive program verification system that combines static and dynamic verification to allow partial specifications. However, because the gradual verifier is a conservative extension of a static verifier, our results also apply to static verifiers that use symbolic execution, such as the Silicon symbolic execution backend for the Viper verification infrastructure used by Gobra, Nagini, and SnaKt.

Figures

Figures reproduced from arXiv: 2607.15383 by the authors.

Figure 1
Figure 1. Predicate definition and usage from the implementation of multi-precision signed integers in Verified [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Checking that a list is sorted [10]. temporarily unfold a predicate, using additional permissions from its body to ensure the evaluation of the expression is framed with sufficient permissions. Without using unfolding expressions in combination with pure functions, specifications are more complex and less intuitive; for instance, in [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Example of unfolding expression. We start with an initial symbolic state with true as the path condition and ∅ as the visited set. Assume we have an object 𝑥 and an initial symbolic heap containing an instance of the pos predicate applied to 𝑥. Note that the symbolic heap doesn’t directly contain a field chunk pertaining to 𝑥.val because it is encapsulated by the predicate pos. We use grey highlights to show the cur… view at source ↗
Figures from the paper (10 more)
Figure 4
Figure 4. Figure 4: Symbolic evaluation rules for unfolding expressions in Viper. [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: Example of pure function. To demonstrate the use of including the post-condition in our approach, we use the post-condition (𝑦.val ≥ 0) =⇒ (result ≥ 𝑥.val), so that it does not directly articulate the same information provided by the implementation. In the program, we …
Figure 6
Figure 6. Figure 6: Symbolic evaluation rules for pure function applications in Viper. [PITH_FULL_IMAGE:figures/full_fig_p009_6.png]
Figure 7
Figure 7. Figure 7: Example of unfolding expression with imprecise predicate. [PITH_FULL_IMAGE:figures/full_fig_p012_7.png]
Figure 8
Figure 8. Figure 8: Symbolic evaluation rules for unfolding expressions in Gradual Viper. [PITH_FULL_IMAGE:figures/full_fig_p013_8.png]
Figure 9
Figure 9. Figure 9: Example of pure function with imprecise precondition. [PITH_FULL_IMAGE:figures/full_fig_p014_9.png]
Figure 10
Figure 10. Figure 10: Example of recursive pure function with imprecise precondition. [PITH_FULL_IMAGE:figures/full_fig_p015_10.png]
Figure 11
Figure 11. Figure 11: Symbolic evaluation rules for pure function applications in Gradual Viper. [PITH_FULL_IMAGE:figures/full_fig_p016_11.png]
Figure 12
Figure 12. Figure 12: Dynamic evaluation and framing rules for unfolding expressions [PITH_FULL_IMAGE:figures/full_fig_p017_12.png]
Figure 13
Figure 13. Figure 13: Dynamic evaluation and framing rules for pure functions [PITH_FULL_IMAGE:figures/full_fig_p017_13.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

34 extracted references · 7 canonical work pages

  1. [1]

    2010.C0, an Imperative Programming Language for Novice Computer Scientists

    Rob Arnold. 2010.C0, an Imperative Programming Language for Novice Computer Scientists. Master’s thesis. Department of Computer Science, Carnegie Mellon University. http://reports-archive.adm.cs.cmu.edu/anon/2010/CMU-CS-10- 145.pdf

    2010

  2. [2]

    Linard Arquint, Malte Schwerhoff, Vaibhav Mehta, and Peter Müller. 2023. A Generic Methodology for the Modular Verification of Security Protocol Implementations. InProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security(Copenhagen, Denmark)(CCS ’23). Association for Computing Machinery, New York, NY, USA, 1377–1391. doi:10.11...

    arXiv 2023

  3. [3]

    Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, Sven N

    Linard Arquint, Felix A. Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, Sven N. Wiesner, David Basin, and Peter Müller. 2023. Sound Verification of Security Protocols: From Design to Interoperable Implementations. In2023 IEEE Symposium on Security and Privacy (SP). IEEE, 1077–1093. doi:10.1109/SP46215.2023.10179325

    arXiv 2023

  4. [4]

    Vytautas Astrauskas, Peter Müller, Federico Poli, and Alexander J. Summers. 2019. Leveraging Rust types for modular specification and verification.Proc. ACM Program. Lang.3, OOPSLA, Article 147 (Oct. 2019), 30 pages. doi:10.1145/ 3360573

    2019

  5. [5]

    Johannes Bader, Jonathan Aldrich, and Éric Tanter. 2018. Gradual Program Verification. InVerification, Model Checking, and Abstract Interpretation. Springer, Los Angeles, CA, USA, 25–46. doi:10.1007/978-3-319-73721-8_2

    work page doi:10.1007/978-3-319-73721-8_2 2018

  6. [6]

    Summers, and Peter Müller

    Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, and Peter Müller. 2025. Formal Foundations for Translational Separation Logic Verifiers.Proc. ACM Program. Lang.9, POPL, Article 20 (Jan. 2025), 31 pages. doi:10.1145/3704856

    work page doi:10.1145/3704856 2025

  7. [7]

    Jenna DiVincenzo, Ian McCormack, Conrad Zimmerman, Hemant Gouni, Jacob Gorenburg, Jan-Paul Ramos-Dávila, Mona Zhang, Joshua Sunshine, Éric Tanter, and Jonathan Aldrich. 2025. Gradual C0: Symbolic Execution for Gradual Verification.ACM Trans. Program. Lang. Syst.46, 4, Article 14 (Jan. 2025), 57 pages. doi:10.1145/3704808 22 Torek et al

    work page doi:10.1145/3704808 2025

  8. [8]

    Marco Eilers and Peter Müller. 2018. Nagini: A Static Verifier for Python. InComputer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing, Cham, 596–603

    2018

Show all 34 references
  1. [9]

    Clark, and Éric Tanter

    Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting Gradual Typing. InProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(St. Petersburg, FL, USA)(POPL ’16). Association for Computing Machinery, New York, NY, USA, 4...

    2016

  2. [10]

    Priyam Gupta. 2025. Increasing the Expressiveness of a Gradual Verifier. arXiv:2507.13533 [cs.PL] https://arxiv.org/ abs/2507.13533

    2025 arXiv

  3. [11]

    Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. InNASA Formal Methods, Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.)....

    2011 doi

  4. [12]

    2023.Verifying Go’s Standard Library

    Adrian Jenny. 2023.Verifying Go’s Standard Library. Practical Work Report. ETH Zürich. https: //ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/ Adrian_Jenny_PW_Report.pdf

    2023

  5. [13]

    Yit Phang Khoo, Bor-Yuh Evan Chang, and Jeffrey S. Foster. 2010. Mixing type checking and symbolic execution. SIGPLAN Not.45, 6 (June 2010), 436–447. doi:10.1145/1809028.1806645

    2010

  6. [14]

    2025.Verifying Parts of the Go Standard Library

    Conradin Laux. 2025.Verifying Parts of the Go Standard Library. Bachelor Thesis. ETH Zürich. https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/ Conradin_Laux_BS_Thesis.pdf

    2025

  7. [15]

    Rustan M

    K. Rustan M. Leino, Peter Müller, and Jan Smans. 2009. Verification of Concurrent Programs with Chalice. In Foundations of Security Analysis and Design V: FOSAD 2007/2008/2009 Tutorial Lectures. Springer, Berlin, Heidelberg, 195–222. doi:10.1007/978-3-642-03829-7_7

    2009 doi

  8. [16]

    Craig Liu. 2024. Design of Fractional Permissions for a Gradual Verifier. InCompanion Proceedings of the 2024 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (Pasadena, CA, USA)(SPLASH Companion ’24). Association...

    2024

  9. [18]

    Doruk Alp Mutlu. 2025. Expanding Specification Capabilities of a Gradual Verifier with Pure Functions. doi:10.48550/ arXiv.2511.22075 arXiv:2511.22075 [cs.PL]

    2025 doi

  10. [19]

    Matthew Parkinson and Gavin Bierman. 2005. Separation logic and abstraction.SIGPLAN Not.40, 1 (Jan. 2005), 247–258. doi:10.1145/1047659.1040326

    2005

  11. [20]

    Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, and Alexander J. Summers. 2024. To- wards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language.Proceedings of the ACM on Programming Langua...

    2024 doi

  12. [21]

    Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix A

    João C. Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix A. Wolf, Marco Eilers, Christoph Sprenger, David Basin, Peter Müller, and Adrian Perrig. 2024. Protocols to Code: Formal Verification of a Next-Generation Internet Router. arXiv:240...

    2024 arXiv

  13. [22]

    2024.Verifying Kotlin Code with Viper by Controlling Aliasing

    Francesco Protopapa. 2024.Verifying Kotlin Code with Viper by Controlling Aliasing. Master’s Thesis. Università degli studi di Padova. https://thesis.unipd.it/retrieve/c1ccf1f6-8073-4b42-abb7-51af9e3518a2/thesis-pdfA.pdf

    2024

  14. [23]

    Reynolds

    John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. InProceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS ’02). IEEE Computer Society, USA, 55–74

    2002

  15. [24]

    2016.Advancing Automated, Permission-based Program Verification Using Symbolic Execution

    Malte Schwerhoff. 2016.Advancing Automated, Permission-based Program Verification Using Symbolic Execution. Ph. D. Dissertation. ETH Zürich

    2016

  16. [25]

    Siek and Walid Taha

    Jeremy G. Siek and Walid Taha. 2007. Gradual Typing for Objects. InECOOP 2007 – Object-Oriented Programming. Springer, Berlin, Germany, 2–27. doi:10.1007/978-3-540-73589-2_2

    2007 doi

  17. [27]

    Jan Smans, Bart Jacobs, and Frank Piessens. 2010. Heap-Dependent Expressions in Separation Logic. InFormal Techniques for Distributed Systems, John Hatcliff and Elena Zucca (Eds.). Springer, Berlin, Heidelberg, 170–185. doi:10. 1007/978-3-642-13464-7_14

    2010

  18. [28]

    Summers and Sophia Drossopoulou

    Alexander J. Summers and Sophia Drossopoulou. 2013. A Formal Semantics for Isorecursive and Equirecursive State Abstractions. InECOOP 2013 – Object-Oriented Programming. Springer, Montpellier, France, 129–153. doi:10.1007/978- 3-642-39038-8_6 Gradually Verifying Unfolding Expr...

    2013 doi

  19. [29]

    Jenna Wise, Johannes Bader, Cameron Wong, Jonathan Aldrich, Éric Tanter, and Joshua Sunshine. 2020. Gradual verification of recursive heap data structures.Proc. ACM Program. Lang.4, OOPSLA, Article 228 (Nov. 2020), 28 pages. doi:10.1145/3428296

    2020 doi

  20. [30]

    Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, João C

    Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, João C. Pereira, and Peter Müller. 2021. Gobra: Modular Specification and Verification of Go Programs. InComputer Aided Verification: 33rd International Conference, CA V 2021, Virtual Event, July 20–23, 2021, Proc...

    2021 doi

  21. [31]

    Wright and Matthias Felleisen

    Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness.Information and Computation 115, 1 (1994), 38–94. doi:10.1006/inco.1994.1093

    1994

  22. [32]

    Conrad Zimmerman, Jenna DiVincenzo, and Jonathan Aldrich. 2024. Sound Gradual Verification with Symbolic Execution.Proc. ACM Program. Lang.8, POPL, Article 85 (Jan. 2024), 30 pages. doi:10.1145/3632927

    2024 doi

  23. [33]

    Conrad Zimmerman, Jenna DiVincenzo, and Jonathan Aldrich. 2024. Sound Gradual Verification with Symbolic Execution.Proceedings of the ACM on Programming Languages8, POPL (Jan. 2024), 2547–2576. https://arxiv.org/abs/ 2311.07559 24 Torek et al. Appendices A Grammar 25 B Run-tim...

    2024 arXiv

  24. [34]

    Part 34.2:We want to show thatΓ ′ corresponds toΣ′ 0

    Therefore Σ′ 0 is reachable from Π with valuation𝑉′ 0 . Part 34.2:We want to show thatΓ ′ corresponds toΣ′ 0. By definition𝑠(Σ′ 0)=body(𝑚); skip=𝑠(Γ ′). Therefore, since𝜎(Σ′ 0)=𝜎 ′ 0, it suffices to show ⟨𝐻, 𝛼′, 𝜌′⟩ 𝑉′ 0 𝜎′ 0. SinceH(𝜎0)=H(𝜎 0)=∅ ,⟨𝐻, 𝛼′\Tpre(𝑚)U⟨𝐻,𝜌′⟩⟩ 𝑉0 H(𝜎...

  25. [35]

    Therefore𝑉′′ 0(𝑔(𝜎′ 0)&&𝑡 0)=𝑉 ′(𝑔(𝜎′ 0))∧𝑉 ′(𝑡′ 0)=true

    Then since⟨𝐻, 𝜌⟩⊢𝑒⇓true , by lemma 28𝑉′′ 0(𝑡0)=true . Therefore𝑉′′ 0(𝑔(𝜎′ 0)&&𝑡 0)=𝑉 ′(𝑔(𝜎′ 0))∧𝑉 ′(𝑡′ 0)=true . Thus, since we have already shown⟨𝐻, 𝛼′, 𝜌⟩ 𝑉′ 0 𝜎′ 0, ⟨𝐻, 𝛼′, 𝜌⟩ 𝑉′′ 0 𝜎′ 0[𝑔=𝑔(𝜎 ′ 0)&&𝑡 0]. Also,𝑠(Σ 0)=𝑠; skipby definition. ThereforeΓ ′ corresponds toΣ 0 with...

  26. [36]

    Part 34.2:Since ⟨𝐻, 𝛼′, 𝜌′⟩⊨ ˜𝜙, by lemma 4 T ˜𝜙U⟨𝐻,𝜌′⟩⊆𝛼′

    Therefore Σ′ 0 is reachable fromΠwith valuation𝑉 ′′ 0 . Part 34.2:Since ⟨𝐻, 𝛼′, 𝜌′⟩⊨ ˜𝜙, by lemma 4 T ˜𝜙U⟨𝐻,𝜌′⟩⊆𝛼′. Also, since the stack is well-formed, 𝛼′ and𝛼 are disjoint, thus𝛼\T ˜𝜙U⟨𝐻,𝜌′⟩ =𝛼 . Therefore⟨𝐻, 𝛼\T ˜𝜙U⟨𝐻,𝜌′⟩, 𝜌⟩ 𝑉′ 0 𝜎′ 0, and now since 𝛼⊆𝛼 ′′, by lemma 19, a...

    2026

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.