Pith. sign in

REVIEW 4 major objections 4 minor 22 references

Modular Verification of Heap Reachability Properties in Separation Logic

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

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

Pith's one-line read Reachability becomes modular when callee footprints are convex

desk verdict Strong DAG framing contribution; the ZOPG field-update criterion has a real macro/Eq.(21) mismatch and a reflexivity problem that need fixing before I'd trust the cyclic part. read the letter →

arxiv 1908.05799 v1 pith:6FHDY343 submitted 2019-08-16 cs.PL cs.LO

Arshavir Ter-Gabrielyan , Alexander J. Summers , Peter Müller This is my paper · ORCID
classification cs.PLcs.LO
keywords reachabilityframingseparationlogicmodularverificationrelativeconvexityfirst-orderSMTsolvers0-1-pathgraphsDAG
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

This paper shows that reachability between heap objects—whether one object can be reached from another along reference chains—can be verified modularly, method by method, if the memory region a method touches is relatively convex inside the caller's region. The authors introduce local reachability predicates and a reachability framing rule that recovers what a callee's effects imply for the caller's larger heap without re-analyzing the whole heap. The technique covers acyclic graphs with bounded outdegree (DAGs such as binary decision diagrams) and cyclic 0-1-path graphs, and it produces proof obligations that SMT solvers handle automatically. Because the reasoning lives inside separation logic, it composes with ordinary permission-based reasoning and with other properties such as sortedness. If the claims hold, automatic verification of graph algorithms such as DAG traversals and ring insertion becomes possible within standard separation-logic tooling.

What carries the argument

The load-bearing device is the relative-convexity condition h ≺ g (Definition 1): footprint h is relatively convex in g if g = f ⊎ h and no path within g leaves h and later returns. This single restriction makes reachability framing first-order: it guarantees a path can cross the boundary between h and f at most once, so the five cases in Fig. 5 (fully inside h, entering h, leaving h, passing through h, or staying in f) are exhaustive. The path partitioning formulas (9) and the frame-localization formulas (15) then serve as the interface between a callee's local reachability summary and the caller's global reachability. Direct field updates are handled by first-order update formulas for adding or removing one edge; for 0-1-path graphs the auxiliary dependency predicate DEP records which edges a path depends on, which is what allows destructive updates to be characterized precisely. The mechanism is sound only while h remains relatively convex after the call, which the method checks at each call site.

What would settle it

Try to verify a sound program whose call satisfies all specifications but whose callee footprint is not relatively convex, such as a method that connects two subgraphs by creating a path that exits and re-enters its own footprint; the paper's post-call convexity check will fail and the proof will be rejected even though the reachability postcondition is true.

Watch

Extended reading notes

Core claim

At the center of the paper is a restriction called relative convexity. A method's footprint h is relatively convex in the caller's footprint g when no path inside g can leave h and later re-enter it (Definition 1). The authors show that under this condition, reachability in the combined heap g = f ⊎ h (frame plus callee region) decomposes exactly into reachability inside h and inside f through five first-order path-partitioning formulas (9), and that reachability local to the frame can be recovered by the frame-localization formulas (15). This converts the reachability framing problem—deducing after a call what paths in the caller's heap survive or are created—into first-order reasoning that SMT solvers can discharge. For direct field updates, the paper adapts incremental transitive-closure update formulas; for cyclic 0-1-path graphs, it introduces an auxiliary dependency relation DEP that tracks which edges a path depends on, enabling precise updates while preserving the 0-1-path invariant through local checks. The method is demonstrated on benchmark programs from prior work, including a recursive DAG merge, left-child-right-sibling encodings, Harris's list, and ring-insertion clients.

Load-bearing premise

The technique only works when every method call's footprint is relatively convex in the caller's footprint—no path inside the caller can leave the callee's region and then re-enter it—and the paper gives no general way to repair call sites that violate this condition.

Editorial extensions

If this is right

  • A method can be verified against reachability specifications by looking only at its own footprint; the callee's postcondition plus the frame-localization formulas give the caller what it needs.
  • Programs with DAGs of bounded outdegree—beyond what previous list-based techniques could handle—become eligible for automatic, SMT-based verification.
  • Cyclic structures such as ring buffers can be handled as 0-1-path graphs, with a local check that each field update or call preserves the 0-1-path invariant.
  • Because reachability is integrated into separation logic, reachability reasoning can be combined with permission-based reasoning for concurrency and with functional specifications such as sortedness.
  • The verification conditions produced by the encoding are first-order, so existing SMT-backed separation-logic verifiers can discharge them without custom decision procedures.

Reading between the lines

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

  • One could try to relax relative convexity by allowing a bounded number of exits and re-entries of the callee footprint; the paper's five-case analysis suggests a route to disjunctive but still first-order framing formulas.
  • If relative convexity is the practical bottleneck, a front-end could attempt to transform non-convex call sites by splitting the callee's footprint into relatively convex pieces or by strengthening the caller's precondition; the paper checks the property but does not explore such transformations.
  • The DEP relation carries strictly more information than plain reachability, so it could serve as a richer specification primitive for cyclic data structures; whether the paper's conversion axioms are always complete for arbitrary ZOPG update sequences is left open.
  • For concurrent programs, read-only permissions on the frame might preserve reachability even when the frame is non-convex; the permission-based separation-logic setting makes this a natural extension of the present technique.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 4 minor

Summary. The paper presents a modular specification and verification technique for heap reachability properties in separation logic. Methods specify reachability locally with respect to a ghost footprint parameter, using edge predicate E and path predicate P. For method calls, the technique requires the callee's footprint to be relatively convex in the caller's footprint (Definition 1) and then provides first-order path-partitioning formulas (Eq. 9) and frame-localized reachability formulas (Eq. 15) to transfer reachability information across calls. For acyclic graphs with bounded outdegree, field updates are handled by adapting the Dong-Su transitive-closure update formulas. For potentially cyclic graphs, the paper extends the technique to 0-1-path graphs (ZOPGs) by introducing an auxiliary DEP relation and incremental criteria for preserving the ZOPG invariant under field updates and method calls. The approach is evaluated by hand-encoding benchmark examples into the Viper verification infrastructure, with a public artifact and a comparison to prior work by Itzhaky et al. and to Flows.

Significance. If the technical claims are correct, this is a significant step beyond prior work: it lifts reachability verification from linked-list structures to arbitrary acyclic bounded-outdegree graphs and to 0-1-path graphs, while remaining in a separation-logic framework that supports permissions, concurrency, and SMT-based automation. The paper's strengths include a concrete public artifact, verification of benchmark examples in Viper, adaptation of known transitive-closure update techniques to a separation-logic setting, and a useful comparison table with prior systems. The main novelty is the use of relative convexity to obtain first-order, precise framing formulas. However, the correctness of the ZOPG part rests on formulas in Section 4 and Appendix B that are internally inconsistent as written, so the cyclic-graph contribution requires substantial revision before the claims can be accepted.

major comments (4)
  1. [§4.2 / App. B] The two formal statements of the ZOPG field-update soundness criterion are inconsistent. Equation (21) requires, for a new edge (u,v), that any x reaching u and any y reached from v satisfy ¬P(g,x,y), i.e., the update must not create an alternative path between arbitrary nodes. The Appendix B macro NO_ALT_PATHS_VIA_EDGE instead concludes ¬P̂(A,α,β) for the endpoints α,β; since the antecedent is satisfied by x=α and y=β, the macro only checks that no path from α to β already exists. Concretely, a ZOPG with edges x→u, v→y, and x→y, and with no path u→v, is accepted by the macro after adding u→v even though two distinct x-to-y paths then exist. If the artifact implements the Appendix B macro, the ZOPG verification is unsound; if it implements Eq. (21), the appendix does not describe the artifact. The manuscript must align the two and state which criterion the public artifact uses.
  2. [§4.2, Eq. (21)] Equation (21) is also too strong as a general ZOPG-preservation condition because P is reflexive and the quantification includes x=y. For an update that closes a directed chain into a simple cycle---a ZOPG-preserving operation---taking x=y to be a node on the chain with P(x,u) and P(v,x) makes the antecedent true, while the consequent ¬P(x,x) contradicts reflexivity. The criterion should either quantify over distinct x≠y or use a suitably non-reflexive reachability relation. The current wording therefore does not correctly characterize when adding an edge preserves the ZOPG property, and it should be repaired before the field-update machinery of Section 4.1 is justified.
  3. [§4.2, Eq. (23)] Equation (23), which formalizes bad configuration (β), contains a duplicated conjunct P0(f,a,/y.alt) and never mentions P0(f,b,/y.alt). As printed, the formula does not express two alternative paths from a and b to /y.alt, so it is not a faithful encoding of Fig. 13(β). Since the four bad configurations in Eqs. (22)–(25) are load-bearing for the method-call ZOPG invariant, this typo must be corrected and the resulting criterion re-validated against the examples and the artifact.
  4. [§4.2, after Eq. (25)] The paper claims that the four configurations in Fig. 13 are complete for violations of the ZOPG invariant after a method call, but only a proof sketch is given. Because the four-case criterion is used to generate proof obligations and is central to the cyclic-graph contribution, the manuscript should provide a rigorous completeness proof, or at least a detailed case analysis that addresses boundary cases such as paths that start and end at the same node and paths that use reflexive reachability. Without this, the soundness of the ZOPG method-call handling is not fully established.
minor comments (4)
  1. [§4.2, Eq. (19)–(25) and throughout] The typesetting contains many OCR artifacts, such as '/y.alt' in place of a variable name and repeated conjuncts; these should be cleaned up in the camera-ready version so that formulas can be checked mechanistically.
  2. [Table 1] The checkmark columns lack a legend: it is not possible to tell which checkmarks correspond to 'greater-than-one outdegree', 'sharing', and 'convex framing' without reading the surrounding text. A column header or caption should clarify this.
  3. [§5.1] The evaluation is based on hand-encoded Viper files rather than an automatic front-end. This is a limitation that should be stated more prominently in the experimental section and in the conclusions, even though a front-end is already listed as future work in §7.
  4. [§3.3] The proof sketch for the merge postcondition omits the explicit relative-convexity checks (Eqs. 11 and 12); including the key instantiations of these checks would make the running example more convincing and would help readers see how the convexity requirement is discharged in practice.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the reachability-framing formulas are derived from relative convexity and external transitive-closure update results, not from the properties they are used to verify.

full rationale

All load-bearing derivation steps are self-contained rather than circular. The path predicates P and DEP are given explicit mathematical meanings (Eqs. 4-5; MetaDefinitionDEP), and the paper's formulas are consequences of those meanings plus the relatively-convex-footprint restriction (Def. 1). Eq. (9) is obtained by an exhaustive case split on how a path in g=f⊎h can interact with h when no path leaves h and later returns; the five cases are not assumed as the definition of P. Eq. (15) likewise follows from relative convexity and the edge/path semantics via a three-way path split around an edge (σ,τ); it is a derived equivalence, not a definition of frame-local reachability in terms of the result being proved. The DEP update formulas are adapted from the external results of Dong and Su [1995], and the DEP conversion axioms in App. C are stated as derivable from the meta-definition; using DEP internally as an encoding does not make P's postconditions defined by the verification outcome. No parameter is fitted to the benchmark examples and then reported as a prediction; the Viper encodings are checked against externally known invariants (merge, reverse, append, Harris list, ring insert). The only self-citations are to the Viper infrastructure and to the artifact, neither of which supplies a load-bearing mathematical premise. The paper explicitly notes in Sec. 4.1 that it plans to investigate the precision limits of the DEP/P conversion, which is an acknowledged limitation rather than a circular justification.

Assumptions & free parameters 0 free parameters · 6 assumptions · 1 invented entities

The paper introduces no free parameters; it relies on prior transitive-closure update results, standard separation-logic machinery, and a set of first-order axioms for the path and DEP relations. The main invented entity is the DEP relation used internally for ZOPG reasoning.

assumptions (6)
  • domain assumption Path predicate P is axiomatized via reflexivity and single-edge unrolling (Eq. 5 in Sec. 3.1).
    The paper leaves P undefined and provides axioms to control SMT quantifier instantiation; soundness relies on this axiomatization approximating true transitive closure.
  • domain assumption Snapshot function postcondition defines the edge set from heap fields (Sec. 3.1).
    Abstraction function from heap to edge set; assumed to capture all relevant field references.
  • standard math Update formulas from Dong and Su [1995] (Eq. 6, App. A, App. B).
    Prior results on first-order transitive-closure updates; the paper adapts them to heaps with reflexivity and extra parameters.
  • domain assumption DEP conversion axioms (PToDep, DepToP, SimplePath, UnrollFromHead, UnrollFromTail, HeadTriangleImposable, TailTriangleImposable, Slingshot, CoalignedEdgeAndPath, App. C).
    Properties of the DEP relation claimed to hold for 0-1-path graphs; derived from MetaDefinitionDEP but assumed as axioms in the verification encoding; paper admits possible imprecision.
  • domain assumption Relative convexity check formulations (Eq. 11, 12) and ZOPG preservation criteria (Eq. 21-25).
    The technique assumes the verifier can establish these formulas from the program's specifications.
  • domain assumption Acyclicity of the footprint is required for field-update formulas in Sec. 3.2.
    The paper asserts ACYCLIC(g) at relevant points (e.g., in updateDAG) and relies on it for the soundness of the reachability update formulas.
invented entities (1)
  • DEPF(g,x,y,u,v)
    purpose: Records that a path from x to y depends on edge (u,v), enabling precise updates for 0-1-path graphs.
    Defined internally via MetaDefinitionDEP; no external falsifiable handle; soundness relies on conversion axioms.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Modular Verification of Heap Reachability Properties in Separation Logic." pith.science (2026). https://pith.science/paper/6FHDY343

@misc{pith2026190805799,
  author       = {Pith},
  title        = {Pith review of: Modular Verification of Heap Reachability Properties in Separation Logic},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/6FHDY343}},
  note         = {Machine review of arXiv:1908.05799}
}
read the original abstract

The correctness of many algorithms and data structures depends on reachability properties, that is, on the existence of chains of references between objects in the heap. Reasoning about reachability is difficult for two main reasons. First, any heap modification may affect an unbounded number of reference chains, which complicates modular verification, in particular, framing. Second, general graph reachability is not supported by SMT solvers, which impedes automatic verification. In this paper, we present a modular specification and verification technique for reachability properties in separation logic. For each method, we specify reachability only locally within the fragment of the heap on which the method operates. A novel form of reachability framing for relatively convex subheaps allows one to extend reachability properties from the heap fragment of a callee to the larger fragment of its caller, enabling precise procedure-modular reasoning. Our technique supports practically important heap structures, namely acyclic graphs with a bounded outdegree as well as (potentially cyclic) graphs with at most one path (modulo cycles) between each pair of nodes. The integration into separation logic allows us to reason about reachability and other properties in a uniform way, to verify concurrent programs, and to automate our technique via existing separation logic verifiers. We demonstrate that our verification technique is amenable to SMT-based verification by encoding a number of benchmark examples into the Viper verification infrastructure.

Figures

Figures reproduced from arXiv: 1908.05799 by the authors.

Figure 1
Figure 1. An example program and specification. Method [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. An example scenario of running merge on two DAGs rooted in l and r. Small circles corre￾spond to heap objects; solid arrows represent fields initialized in the pre-state that are unchanged; the dashed arrow represents the new heap edge (created in the post-state by initializing a field). The frame of the recursive call is surrounded with blue; the footprint is surrounded with red. could easily provide a less abstrac… view at source ↗
Figure 3
Figure 3. The reachability update problem in presence of alter [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figures from the paper (10 more)
Figure 4
Figure 4. Figure 4: The flow of reachability information in the presence [PITH_FULL_IMAGE:figures/full_fig_p009_4.png]
Figure 5
Figure 5. Figure 5: No paths originating and ending inside a relatively c [PITH_FULL_IMAGE:figures/full_fig_p010_5.png]
Figure 6
Figure 6. Figure 6: The footprint (surrounded with red) is relatively co [PITH_FULL_IMAGE:figures/full_fig_p011_6.png]
Figure 7
Figure 7. Figure 7: Encoding merge in Viper. Types are translated directly. The specifications (Sec. 2.1) are omi ed for brevity. The reference field update is translated via unlinkDAG, linkDAG (Sec. 3.2). The method call is augmented with local assumptions in the form of macros (lines st…
Figure 8
Figure 8. Figure 8: The method joinAndModify first a aches the hammock h to the hammock f, creating a larger hammock, and then calls the method disconnectAll, creating a frame that is non-convex in g. Ver￾ification of the postcondition is challenging, as it requires localizing reachabilit…
Figure 9
Figure 9. Figure 9: Paths starting and ending in the frame of a relatively [PITH_FULL_IMAGE:figures/full_fig_p015_9.png]
Figure 10
Figure 10. Figure 10: An example scenario of running the method [PITH_FULL_IMAGE:figures/full_fig_p016_10.png]
Figure 11
Figure 11. Figure 11: An example client with a ZOPG footprint. For simplic [PITH_FULL_IMAGE:figures/full_fig_p020_11.png]
Figure 12
Figure 12. Figure 12: A typical scenario of running testZopgObligations. r is an arbitrary node of the ring, and u is added to the ring a er the call to ringInsert. The diagram demonstrates a data structure with nodes that can have two reference fields (for simplicity, the implementation o…
Figure 13
Figure 13. Figure 13: The four configurations that violate the ZOPG invar [PITH_FULL_IMAGE:figures/full_fig_p022_13.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

22 extracted references · 22 canonical work pages

  1. [2]

    https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/ K

    (2008). https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/ K. Rustan M. Leino and Rosemary Monahan

    work page 2008

  2. [3]

    We denote the footprint of the method enclosing this field update as g

    Our goal is to rewrite operations of the form from.f := to in such a way that would introduce reachability update formulas [Dong and Su 1995] to the verifier. We denote the footprint of the method enclosing this field update as g. We assume that this methods implementation and specification mentions reference fields from the set F ; in particular, f ∈ F . Sin...

    work page 1995

  3. [4]

    We assume that the reader understand the previous case of DAGs discussed in App. A; similarly, our goal now is to rewrite operations of the form from.f := to in such a way that would introduce precise update formulas to the verifier, except this time we a re interested in the auxiliary DEP relation for ZOPGs (and notP). As before, we denote the footprint o...

    work page 2019

  4. [11]

    ACM International Conference Proceeding Series (2009)

    Programming with triggers. ACM International Conference Proceeding Series (2009). Peter Müller

    work page 2009

  5. [12]

    In Principled Software Development , Peter Müller and Ina Schaefer (Eds.)

    The Binomial Heap Verification Challenge in Viper . In Principled Software Development , Peter Müller and Ina Schaefer (Eds.). Springer-Verlag, 203–219. Peter Müller, Malte Schwerhoff, and Alexander J. Summers. 2016 a. Automatic Verification of Iterated Separating Conjunc- tions using Symbolic Execution. In CA V (LNCS), Swarat Chaudhuri and Azadeh Farzan (Eds.), Vol

    work page 2016

  6. [19]

    The dire ct update formulas provide a canonical form of the reachability relation in the new state (e

    consider an irreflexive transitive closure relation. The dire ct update formulas provide a canonical form of the reachability relation in the new state (e. g., P ⇔ ( . . .)) based on the reach- ability relation in the old state (e.g., (. . .) ⇔ Q[P0], where Q[R] is a first-order formula over R). Finally, we exploit the fact that both unlinkDAG and linkDAG r...

    work page 1995

  7. [21]

    Page 33 of 1–34

    2019-08-19 00:46. Page 33 of 1–34. 34 Arshavir Ter-Gabrielyan, Alexander J. Summers, and Peter Mü ller Appendix C CONVERSION RULES FOR THE DEP RELATION The auxiliary DEP relation enables precise reasoning about reachability in 0–1- path graphs. How- ever, the formal definition of DEP3 is beyond first-order logic: ∀x,/y.alt,u,/v.alt• DEP(x,/y.alt,u,/v.alt) ....

    work page 2019

  8. [22]

    2019-08-19 00:46

    3Note that here we omit the first parameter (i.e., the sub-heap) inall relation symbols as it is implicitly universally quantified and the same in all formulas. 2019-08-19 00:46. Page 34 of 1–34

    work page 2019

Show all 22 references
  1. [1958]

    Operations Research 6, 6 (1958), 791–812

    A Method for Solving Traveling-Salesman Probl ems. Operations Research 6, 6 (1958), 791–812. Leonardo Mendonça de Moura and Nikolaj Bjørner

    1958

  2. [1959]

    The Bell System Technical Journal 38, 4 (1959), 985–999

    Representation of switching circuits by binary-decisio n programs. The Bell System Technical Journal 38, 4 (1959), 985–999. K Rustan M Leino

    1959

  3. [1965]

    The Bell System Technical Journal 44, 10 (1965), 2245–2269

    Computer solutions of the traveling salesman probl em. The Bell System Technical Journal 44, 10 (1965), 2245–2269. Michal Moskal

    1965

  4. [1975]

    Journal of the ACM 22, 2 (1975), 215–225

    Efficiency of a Good But Not Linear Set Union A lgorithm. Journal of the ACM 22, 2 (1975), 215–225. Arshavir Ter-Gabrielyan, Alexander J. Summers, and Peter Müller

    1975

  5. [1978]

    IEEE Trans

    Binary Decision Diagrams. IEEE Trans. Comput. 27, 6 (1978), 509–516. Clark Barrett, Pascal Fontaine, and Cesare Tinelli

    1978

  6. [1986]

    Algorithmica 1 (1986), 111–129

    The pairing heap: A new form of self-adjusting heap. Algorithmica 1 (1986), 111–129. Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Alek sandar Nanevski, and Mooly Sagiv

    1986

  7. [1990]

    IEEE Trans

    Prior ity inheritance protocols: an approach to real-time synchronization. IEEE Trans. Comput. 39, 9 (1990), 1175–1185. Jan Smans, Bart Jacobs, and Frank Piessens

    1990

  8. [1995]

    Incremental and Decremental Evaluation of Transitive Closure by First-Order Queries. Inf. Comput. 120 (1995), 101–106. Michael L. Fredman, Robert Sedgewick, Daniel Dominic Sleator, and Rob ert E. Tarjan

    1995

  9. [2005]

    Journal of the ACM 52, 3 (2005), 365–473

    Simplify: A Th eorem Prover for Program Checking. Journal of the ACM 52, 3 (2005), 365–473. Guozhu Dong and Jianwen Su

    2005

  10. [2009]

    Logical Methods in Computer Science 5, 2 (2009)

    Simulating reach- ability using first-order logic with applications to verification of linked data structures. Logical Methods in Computer Science 5, 2 (2009). Shen Lin

    2009

  11. [2011]

    In ESOP, Gilles Barthe (Ed.)

    The Relations hip between Separation Logic and Implicit Dynamic Frames. In ESOP, Gilles Barthe (Ed.). 439–458. 2019-08-19 00:46. Page 28 of 1–34. Modular Verification of Heap Reachability Properties in Sep aration Logic 29 Ruzica Piskac, Thomas Wies, and Damien Zufferey

    2019

  12. [2012]

    ACM Transactions on Programming Languages and Systems 34, 1, Article 2 (2012), 58 pages

    Implicit Dynamic Fra mes. ACM Transactions on Programming Languages and Systems 34, 1, Article 2 (2012), 58 pages. Robert Endre Tarjan

    2012

  13. [2018]

    PACMPL 2, POPL (2018), 37:1–37:31

    Go with the flow: compositional abstractions for concurrent data structures. PACMPL 2, POPL (2018), 37:1–37:31. C. Y. Lee

    2018

  14. [2019]

    https://doi.org/10.5281/zenodo.3367478 Hongseok Yang

    Modular Verification of Heap Reachability Prop- erties in Separation Logic (Artifact). https://doi.org/10.5281/zenodo.3367478 Hongseok Yang. 2001a. An example of local reasoning in BI pointer logic : the Schorr-Waite graph marking algorithm. In Proceedings of the SPACE Workshop...

    doi

Pith tools

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