Pith. sign in

REVIEW 2 major objections 6 minor 2 cited by

Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic

T0 review · 2 major / 6 minor · reviewed 2026-08-16 · deepseek-v4-flash

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

Pith's one-line read A single assertion encoding reduces ∀∃ relational Hoare logic to standard Hoare logic, proved under a relaxed refinement semantics.

desk verdict A clean, machine-checked encoding of a relaxed ∀∃ relational Hoare logic into standard Hoare logic; the title overstates the semantics, but the contribution is real and worth reviewing. read the letter →

arxiv 2504.17444 v2 pith:GIKNCCLI submitted 2025-04-24 cs.PL

Shushu Wu , Xiwei Wu , Qinxiang Cao This is my paper · ORCID
classification cs.PL MSC 68Q6003B70
keywords relationalHoarelogicprogramrefinementnondeterminismassertionencodingweakestpreconditionconfigurationprogram-as-resourceassertionsexecutionpredicate
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

The paper claims that the $\forall\exists$ relational Hoare logic used to prove refinement of nondeterministic programs can be embedded faithfully in ordinary standard Hoare logic, with no ghost states or invariant machinery. The key move is to redefine relational-triple validity using configuration refinement, a denotational inclusion of possible outcomes, instead of multi-step small-step transitions, and then to encode each program-as-resource assertion as a unary assertion over low-level states that existentially abstracts the high-level state and remaining high-level program. The main theorem states that a relational triple is valid exactly when every encoded standard triple, universally parameterized by a high-level postcondition $X$, is $\forall$-valid. A syntactic form of the encoding uses a pure execution predicate $\mathrm{Exec}_X(P^H,c^H)$ that the low-level proof can carry along with ordinary Hoare rules, so relational proof rules become derivable standard rules. If the encoding is right, existing standard-Hoare verification infrastructure can prove refinement without building or re-verifying a second program logic.

What carries the argument

The load-bearing object is configuration refinement: $(\sigma_1,c_1)\hookrightarrow(\sigma_2,c_2)$ holds exactly when every terminal state reachable from $(\sigma_2,c_2)$ by denotational semantics is reachable from $(\sigma_1,c_1)$. Its decomposition theorem is what makes the encoding work: $(\sigma_1,c_1)\hookrightarrow(\sigma_2,c_2)$ is equivalent to $\forall X\subseteq\Sigma^H.\ \sigma_1\models\mathrm{wlp}(c_1,X)\Rightarrow \sigma_2\models\mathrm{wlp}(c_2,X)$. Because a refinement step becomes a universal implication over weakest preconditions, the existential 'choose a matching high-level execution' can be absorbed into the assertion encoding $\llbracket\cdot\rrbracket_X$. The syntactic encoding introduces the pure execution predicate $\mathrm{Exec}_X(P^H,c^H)$, read as 'there is a high-level state satisfying $P^H$ from which every $c^H$ outcome satisfies $X$'; proof rules update this predicate to emulate high-level evaluation steps.

What would settle it

Run the paper's own counterexample: under the original multi-step semantics, the triple $\langle x = y \land [\mathbf{skip}]\rangle\, x := x+1\,\langle x = y \land [y := y-1]\rangle$ is invalid because there is no small-step path from the initial configuration to the final configuration, while the configuration-refinement definition declares it valid and Theorem 4 proves the encoded standard triple.

Watch

Extended reading notes

Core claim

The central discovery is Theorem 4: for any low-level statement $c^L$ and program-as-resource assertions $\mathcal{P},\mathcal{Q}$, the relational triple $\langle\mathcal{P}\rangle\,c^L\,\langle\mathcal{Q}\rangle$ is valid if and only if, for every high-level state set $X$, the standard triple $\{\llbracket\mathcal{P}\rrbracket_X\}\,c^L\,\{\llbracket\mathcal{Q}\rrbracket_X\}$ is $\forall$-valid. The encoding is $\sigma^L \models \llbracket\mathcal{P}\rrbracket_X$ iff there exist $\sigma^H,c^H$ with $(\sigma^L,\sigma^H,c^H)\models\mathcal{P}$ and $\sigma^H\models\mathrm{wlp}(c^H,X)$. This turns the existential choice inside a relational proof into an existential quantifier inside an assertion, which standard Hoare logic can handle. The equivalence is proved under Definition 9, where the high-level update relation is configuration refinement rather than multi-step transition; the authors explicitly note that this relaxed validity makes some previously invalid triples valid, while preserving the intended refinement reading when the postcondition program is $\mathbf{skip}$.

Load-bearing premise

The central equivalence assumes the relaxed definition of relational validity via configuration refinement; under the original multi-step-transition semantics, the theorem as stated is not expected to hold.

Editorial extensions

If this is right

  • Any verification infrastructure for standard Hoare logic can prove refinement triples by adding the execution predicate, without re-proving soundness of a second logic.
  • Relational proof rules for sequencing, loops, nondeterministic choice, and the two vertical-composition rules become derivable standard rules, so relational proof steps correspond one-for-one to standard proof steps.
  • The placeholder $X$ is inert in practice: proofs operate on $\mathrm{Exec}_X(P^H,c^H)$ by update rules, so users never need to construct $X$ explicitly.
  • The encoding extends to function calls, error behaviour, and separation-logic frame reasoning while preserving the same equivalence.

Reading between the lines

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

  • The relaxed validity trades exact trace alignment for denotational behaviour: refinement conclusions are about possible final results, not about matching every small step; full refinement still requires the postcondition program to be $\mathbf{skip}$, but intermediate continuations in assertions are interpreted coarser than before.
  • A testable extension is to specialize the universal placeholder $X$ to the weakest precondition of a concrete high-level postcondition, yielding a proof rule for known input-output refinement that may recover exact small-step validity when the high-level language is deterministic.
  • The encoding suggests that adding an execution predicate to an existing unary verifier is a modular route to refinement checking; one could compare proof effort and automation against ghost-state-based refinement logics on the heap-manipulating case studies.
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

2 major / 6 minor

Summary. The paper proposes an encoding theory that reduces a programs-as-resources relational Hoare logic for nondeterministic programs to standard (unary) Hoare logic. It redefines relational triple validity using a configuration-refinement relation based on denotational semantics rather than multi-step transitions, then defines an assertion encoding L·M_X via weakest preconditions. Theorem 4 states that a relational triple is valid under this relaxed semantics iff, for every high-level postcondition X, the encoded standard Hoare triple is ∀-valid. The paper also gives a syntactic encoding using an execution predicate Exec_X, presents proof rules for this predicate, shows how relational proof rules become standard proof rules, and reports machine-checked Rocq formalization plus case studies including mergesort, BST, DFS, and KMP.

Significance. Within its redefined semantics, the encoding is elegant and theoretically useful: it avoids ghost-state and invariant machinery, and it allows standard Hoare logic proof infrastructure to be reused for refinement proofs. The paper's strengths include a semantic proof of the central equivalence, a machine-checked Rocq formalization with a Zenodo artifact, and substantial case studies. The authors are also transparent in Section 8 that configuration refinement is a weakening of multi-step validity and that some previously invalid triples become valid. The main limitation is that Theorem 4 does not encode the original Definition 1 semantics; because the encoded standard triple does not depend on the relational semantics, the equivalence is exact only for the relaxed logic. For final refinement judgments with [skip] postconditions, Proposition 10 recovers the original meaning, but intermediate judgments in relational proofs are broader, so the advertised scope of the title and abstract should be adjusted.

major comments (2)
  1. [§3 (Definition 9), §4 (Theorem 4), §8] Theorem 4 is proved for the relaxed validity based on configuration refinement ↩→, not for the original multi-step validity of Definition 1. The example in Section 8, ⟨x = y ∧ [skip]⟩ x := x+1 ⟨x = y ∧ [y := y−1]⟩, is valid under Definition 9 but invalid under Definition 1, and since the encoded standard triple is ∀-valid independently of which relational semantics is fixed, the theorem would be false for Definition 1. This gap is load-bearing for the paper's central claim: the title and abstract present the result as an encoding of the ∀∃ relational Hoare logic, and intermediate rules such as Rel-Seq and High-Focus can derive triples that are valid only under the relaxed semantics. Proposition 10 rescues only the fragment whose postcondition is [skip]. I request that the paper be explicitly rescoped—in the title, abstract, and introduction—to the configuration-refinement-based validity, with a precise statement that the original multi-step semantics is encoded only for the [skip]-postcondition refinement fragment.
  2. [§4.2 (Theorem 4), §5.2 (Definition 17)] The theorem's right-hand side universally quantifies over an arbitrary subset X of high-level states, and the assertion encoding L·M_X and Exec_X are parameterized by this second-order object. The paper argues in Section 8 that X is a mere placeholder and compares it to logical variables in VST specifications, but VST-style logical variables range over data values, not over sets of states. The text should state more precisely that using the encoding in a concrete standard Hoare logic requires either a schematic meta-level variable X or an assertion language extended with a family of predicates indexed by X; otherwise the reduction is a meta-theorem rather than a syntactic judgment in the underlying object logic. This is a clarification of the practical scope of the reduction rather than a challenge to the semantic argument.
minor comments (6)
  1. [§4.2 and Appendix B (Theorem 4 proof, ⇐ direction)] In the sentence 'That is for any σH3 such that (σH2,σH3)∈JcH2Knrm, we have (σH1,σH3)∈JcH2Knrm', the second occurrence of JcH2Knrm should be JcH1Knrm; the same typo appears in the appendix proof.
  2. [§5.2 vs. Appendix C.2] The numbering 'Definition 17' is used twice: once for the syntactic encoding in Section 5.2 and once for the semantic interpretation of the execution predicate in Appendix C.2. Please renumber so that cross-references are unambiguous.
  3. [§7.1 (Figure 10)] The high-level mergeH code is misparenthesized and hard to parse; the two branches of the choice construct are not clearly delimited. Please rewrite the pseudocode with explicit begin/end or indentation for each branch.
  4. [§5.1 (Theorem 16(d), proof)] The proof of the disjunction case begins with 'we have ∃𝑎.∃σH cH...' even though no existential variable 𝑎 is involved in that case; remove the stray ∃𝑎 or correct the formula to match the disjunction case.
  5. [§6.1 (Figure 9, Exec-Nondet)] The side condition of Exec-Nondet is written as 'P_H[v/x] ⇒ e1≤v≤e2' without explicit quantification over v. State whether this is meant universally over all v or for the value chosen by the nondeterministic assignment, since this affects how the rule is applied.
  6. [Abstract and §1] The phrase 'without requiring modifications to the logic framework' is stronger than what is demonstrated: the paper introduces the Exec_X predicate and its update rules into the assertion language and proof system. Suggest wording such as 'without changing the core standard Hoare rules or re-verifying their soundness.'

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Theorem 4 is a direct semantic correspondence proved from independent definitions, with only a disclosed scope limitation regarding the redefined validity relation.

full rationale

The derivation in Theorem 4 is self-contained: Definition 9 (relaxed relational validity via configuration refinement) and Definition 15 (assertion encoding via weakest preconditions) are independent semantic definitions, and the equivalence is proved by expanding configuration refinement (Def. 7) through weakest preconditions (Def. 12), using Theorem 11 and the set-theoretic Proposition 13/14. The high-level program does not appear in the assumptions in a way that forces the conclusion; the placeholder X is instantiated in the reverse direction with the terminal-state set of the initial high-level configuration, which is a legitimate proof technique rather than a circular step. The main proof rules (Low-Focus, High-Focus, Rel-Wh, Choice) are re-derived as standard Hoare rules from the encoding, not assumed as the target. Self-citations (e.g., the QCP tool [47] and the Rocq artifact [46]) are used as implementation and formalization evidence, not as load-bearing justification for the encoding theorem. The paper explicitly discloses in Sec. 8 that it redefines relational triple validity using configuration refinement instead of multi-step transitions, giving the example ⟨x = y ∧ [skip]⟩ x := x+1 ⟨x = y ∧ [y := y-1]⟩; therefore Theorem 4 is an exact correspondence for the relaxed judgment of Definition 9, not for the original multi-step Definition 1. This is a scope limitation openly acknowledged by the authors, not a circular reduction of the theorem to its own inputs.

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

The central encoding theorem rests on the semantic framework (denotational semantics) and on the newly introduced configuration refinement relation. No free parameters are fitted; no new physical or logical entities are postulated beyond the definition of the execution predicate.

assumptions (3)
  • domain assumption Programs are equipped with denotational semantics JcK_nrm (Definition 6).
    The entire development, including configuration refinement and weakest preconditions, is built on denotational semantics. The paper states this at the start of Sec. 3.
  • domain assumption Small-step multi-step transitions and denotational semantics characterize the same high-level behavior (Proposition 5).
    Used to connect the relational triple's small-step formulation to the denotational one; the authors assume this consistency.
  • ad hoc to paper The relaxed configuration refinement relation ↩→ is an adequate substitute for multi-step transitions in the definition of valid relational triples (Definition 9).
    This is the key weakening the paper introduces. It makes some previously invalid triples valid (Sec. 8), and the encoding theorem is proved with respect to this weakened semantics.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic." pith.science (2026). https://pith.science/paper/GIKNCCLI

@misc{pith2026250417444,
  author       = {Pith},
  title        = {Pith review of: Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GIKNCCLI}},
  note         = {Machine review of arXiv:2504.17444}
}
abstract

Verifying a real-world program's functional correctness can be decomposed into (1) a refinement proof showing that the program implements a more abstract high-level program and (2) an algorithm correctness proof at the high level. Relational Hoare logic serves as a powerful tool to establish refinement but often necessitates formalization beyond standard Hoare logic. Particularly in the nondeterministic setting, the $\forall\exists$ relational Hoare logic is required. Existing approaches encode this logic into a Hoare logic with ghost states and invariants, yet these extensions significantly increase formalization complexity and soundness proof overhead. This paper proposes a generic encoding theory that reduces the $\forall\exists$ relational Hoare logic to standard (unary) Hoare logic. Precisely, we propose to redefine the validity of relational Hoare triples while preserving the original proof rules and then encapsulate the $\forall\exists$ pattern within assertions. We have proved that the validity of encoded standard Hoare triples is equivalent to the validity of the desired relational Hoare triples. Moreover, the encoding theory demonstrates how common relational Hoare logic proof rules are indeed special cases of standard Hoare logic proof rules, and relational proof steps correspond to standard proof steps. Our theory enables standard Hoare logic to prove $\forall\exists$ relational properties by defining a predicate Exec, without requiring modifications to the logic framework or re-verification of soundness.

Figures

Figures reproduced from arXiv: 2504.17444 by the authors.

Figure 1
Figure 1. Relational Hoare Triples 1 L ≾ ≾ 1 H 2 L 2 H [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 3
Figure 3. The bitmask/set example: a low-level program uses bitmask operations to record constants, a high-level [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figure 4
Figure 4. Proof Rules in Relational and Standard Hoare logic [PITH_FULL_IMAGE:figures/full_fig_p004_4.png] view at source ↗
Figures from the paper (9 more)
Figure 5
Figure 5. Figure 5: Relational and standard proofs for the bitmask/set example. [PITH_FULL_IMAGE:figures/full_fig_p005_5.png]
Figure 6
Figure 6. Figure 6: Core Relational Proof Rules 2.1 High-level Programs as Resources Treating high-level programs as resources involves extending a binary assertion P ⊆ Σ L ×Σ H with a high-level program 𝑐 H ∈ ProgH. Here, Σ L and Σ H represent the set of low-level program states and the …
Figure 7
Figure 7. Figure 7: State Transition Relation. It is worth noting that the reverse implication does not necessarily hold. For instance, we can show that (x = 0,skip) ↩→ (x = 1, x := x − 1), whereas there is no multi-step transition from the left configuration to the right one. Based on co…
Figure 8
Figure 8. Figure 8: Low-level Dependent Relational rules and their corresponding encoded rules [PITH_FULL_IMAGE:figures/full_fig_p015_8.png]
Figure 9
Figure 9. Figure 9: Proof rules for Evaluating High-level Programs [PITH_FULL_IMAGE:figures/full_fig_p016_9.png]
Figure 10
Figure 10. Figure 10: The merge example: the low-level program (left) merges two singly linked lists using explicit pointer [PITH_FULL_IMAGE:figures/full_fig_p020_10.png]
Figure 11
Figure 11. Figure 11: Relational Hoare Triples Subsequent frameworks [19, 38, 39] leverage this (∀∃)𝜔 Hoare logic to encode the ∀∃ relational Hoare logic for verifying program refinement. A common strategy is to instantiate the ghost state as a high-level program configuration and set the …
Figure 12
Figure 12. Figure 12: Implementations of recording a collection with arrays [PITH_FULL_IMAGE:figures/full_fig_p035_12.png]
Figure 13
Figure 13. Figure 13: Refinement Proof Based on Standard Hoare triples [PITH_FULL_IMAGE:figures/full_fig_p038_13.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Forall-Exists Relational Verification by Filtering to Forall-Forall

    cs.LO 2025-09 conditional novelty 7.0 of 10

    A sound filter-adequacy transformation proves that verifying a forall-forall property of a transformed bicom implies the original forall-exists property.

  2. A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms

    cs.PL 2025-04 conditional novelty 7.0 of 10

    A state relation monad plus a two-stage proof style lets algorithms like DFS and KMP be specified and verified in Coq with proofs organized by logical structure.

Reference graph

Works this paper leans on

83 extracted references · 44 canonical work pages · cited by 2 Pith papers

  1. [1]

    Aho, Catriel Beeri, and Jeffrey D

    Alfred V. Aho, Catriel Beeri, and Jeffrey D. Ullman. 1979. The Theory of Joins in Relational Databases. ACM Trans. Database Syst. 4, 3 (1979), 297–314. doi:10.1145/320083.320091

    arXiv 1979

  2. [2]

    Naumann, and Minh Ngo

    Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo

  3. [3]

    Andrew W. Appel. 2012. Verified Software Toolchain.. In NASA Formal Methods (Lecture Notes in Computer Science, Vol. 7226), Alwyn Goodloe and Suzette Person (Eds.). Springer, 2. http://dblp.uni-trier.de/db/conf/nfm/nfm2012.html# Appel12

    2012

  4. [4]

    Andrew W. Appel. 2022. Coq’s vibrant ecosystem for verification engineering (invited talk). In CPP ’22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022 , Andrei Popescu and Steve Zdancewic (Eds.). ACM, 2–11. doi:10.1145/3497775.3503951

    arXiv 2022

  5. [5]

    Naumann, and Mohammad Nikouei

    Anindya Banerjee, Ramana Nagasamudram, David A. Naumann, and Mohammad Nikouei. 2022. A Relational Program Logic with Data Abstraction and Dynamic Framing. ACM Trans. Program. Lang. Syst. 44, 4 (2022), 25:1–25:136. doi:10.1145/3551497

    doi:10.1145/3551497 2022

  6. [6]

    Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2013. Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification. In Logical Foundations of Computer Science, International Symposium, LFCS 2013, San Diego, CA, USA, January 6-8, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 7734) , Sergei N. Artëmov and Anil Nerode (Eds...

    doi:10.1007/978-3-642-35722-0_3 2013

  7. [7]

    Barthe, P.R

    G. Barthe, P.R. D’Argenio, and T. Rezk. 2004. Secure information flow by self-composition. In Proceedings. 17th IEEE Computer Security Foundations Workshop, 2004. 100–114. doi:10.1109/CSFW.2004.1310735

    arXiv 2004

  8. [8]

    Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations. InProceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, Neil D. Jones and Xavier Leroy (Eds.). ACM, 14–25. doi:10.1145/964001.964003

    arXiv 2004

Show all 83 references
  1. [9]

    Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. 2018. VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. J. Autom. Reason. 61, 1-4 (2018), 367–422. doi:10.1007/S10817-018- 9457-5

    2018 doi

  2. [10]

    Martin Clochard, Claude Marché, and Andrei Paskevich. 2020. Deductive verification with ghost monitors. Proc. ACM Program. Lang. 4, POPL (2020), 2:1–2:26. doi:10.1145/3371070

    2020 doi

  3. [11]

    Thibault Dardinier, Anqi Li, and Peter Müller. 2024. Hypra: A Deductive Program Verifier for Hyper Hoare Logic. Proc. ACM Program. Lang. 8, OOPSLA2 (2024), 1279–1308. doi:10.1145/3689756

    2024 doi

  4. [12]

    Thibault Dardinier and Peter Müller. 2023. Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version). CoRR abs/2301.10037 (2023). doi:10.48550/ARXIV.2301.10037 arXiv:2301.10037

    2023 doi arXiv

  5. [13]

    Willem-Paul de Roever and Kai Engelhardt. 1998. Simulation and Hoare Logic . Cambridge University Press, 132–145

    1998

  6. [14]

    Zhang, and Benjamin Delaware

    Robert Dickerson, Qianchuan Ye, Michael K. Zhang, and Benjamin Delaware. 2022. RHLE: Modular Deductive Verification of Relational∀∃ Properties. In Programming Languages and Systems - 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings (Lectur...

    2022 doi

  7. [15]

    Edsger Wybe Dijkstra. 1997. A Discipline of Programming (1st ed.). Prentice Hall PTR, USA

    1997

  8. [16]

    Emanuele D’Osualdo, Azadeh Farzan, and Derek Dreyer. 2022. Proving hypersafety compositionally. Proc. ACM Program. Lang. 6, OOPSLA2, Article 135 (Oct. 2022), 26 pages. doi:10.1145/3563298

    2022 doi

  9. [17]

    Jean-Christophe Filliâtre and Andrei Paskevich. 2013. Why3: where programs meet provers. In Proceedings of the 22nd European Conference on Programming Languages and Systems (Rome, Italy) (ESOP’13). Springer-Verlag, Berlin, Heidelberg, 125–128. doi:10.1007/978-3-642-37036-6_8

    2013 doi

  10. [18]

    Robert W. Floyd. 1967. Assigning Meanings to Programs. Proceedings of Symposium on Applied Mathematics 19 (1967), 19–32. http://laser.cs.umass.edu/courses/cs521-621.Spr06/papers/Floyd.pdf

    1967

  11. [19]

    Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2020. ReLoC Reloaded: A Mechanized Relational Logic for Fine- Grained Concurrency and Logical Atomicity. CoRR abs/2006.13635 (2020). arXiv:2006.13635 https://arxiv.org/abs/ 2006.13635

    2020 arXiv

  12. [20]

    Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. 2022. Simuliris: a separation logic framework for verifying concurrent program optimizations. Proc. ACM Program. Lang. 6, POPL (2022), 1–31. doi:10.1145/3498689

    2022 doi

  13. [21]

    Lorch, Bryan Parno, Michael Lowell Roberts, Srinath T

    Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael Lowell Roberts, Srinath T. V. Setty, and Brian Zill. 2015. IronFleet: proving practical distributed systems correct. InProceedings of the 25th Symposium on Operating Systems Principles, SOSP 20...

    2015

  14. [22]

    C. A. R. Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (oct 1969), 576–580. doi:10.1145/363235.363259

    1969

  15. [23]

    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. In NASA Formal Methods, Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.)...

    2011

  16. [24]

    Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018), e20. doi:10.1017/S0956796818000151

    2018 doi

  17. [25]

    Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Progra...

    2015

  18. [26]

    Sudipta Kundu, Zachary Tatlock, and Sorin Lerner. 2009. Proving optimizations correct using parameterized program equivalence. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, June 15-21, 2009 , Mi...

    2009 doi

  19. [27]

    Peter Lammich and René Neumann. 2015. A framework for verifying depth-first search algorithms. In Proceedings of the 2015 Conference on Certified Programs and Proofs . 137–146

    2015

  20. [28]

    Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs using Linear Ghost Types. Proc. ACM Program. Lang. 7, OOPSLA1, Article 85 (April 2023), 30 pages. doi:10.1...

    2023 doi

  21. [29]

    Rustan M

    K. Rustan M. Leino. 2010. Dafny: an automatic program verifier for functional correctness. In Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (Dakar, Senegal) (LPAR’10). Springer-Verlag, Berlin, Heidelberg, 348–370

    2010

  22. [30]

    Hongjin Liang and Xinyu Feng. 2013. Modular verification of linearizability with non-fixed linearization points. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, W A, USA, June 16-19, 2013, Hans-Juergen Boehm and Cormac Flanagan (...

    2013

  23. [31]

    Hongjin Liang and Xinyu Feng. 2016. A program logic for concurrent objects under fair scheduling. InProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016 , Rastislav Bodík a...

    2016

  24. [32]

    Kenji Maillard, Catalin Hritcu, Exequiel Rivas, and Antoine Van Muylder. 2020. The next 700 relational program logics. Proc. ACM Program. Lang. 4, POPL (2020), 4:1–4:33. doi:10.1145/3371072

    2020 doi

  25. [33]

    Ramana Nagasamudram and David A. Naumann. 2021. Alignment Completeness for Relational Hoare Logics. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021 . IEEE, 1–13. doi:10.1109/LICS52264.2021.9470690

    2021

  26. [34]

    David A. Naumann. 2020. Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and History. In Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Met...

    2020

  27. [35]

    Peter W. O’Hearn. 2020. Incorrectness logic. Proc. ACM Program. Lang. 4, POPL (2020), 10:1–10:32. doi:10.1145/3371078

    2020 doi

  28. [36]

    Reynolds

    John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings . IEEE Computer Society, 55–74. doi:10.1109/LICS.2002.1029817

    2002 arXiv

  29. [37]

    Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer. 2023. Conditional Contextual Refinement. Proc. ACM Program. Lang. 7, POPL (2023), 1121–1151. doi:10.1145/3571232

    2023 doi

  30. [38]

    Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, and Lars Birkedal

  31. [39]

    Joseph Tassarotti, Ralf Jung, and Robert Harper. 2017. A Higher-Order Logic for Concurrent Termination-Preserving Refinement. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and ...

    2017 doi

  32. [40]

    Tachio Terauchi and Alex Aiken. 2005. Secure Information Flow as a Safety Problem.. InSAS (Lecture Notes in Computer Science, Vol. 3672), Chris Hankin and Igor Siveroni (Eds.). Springer, 352–367. http://dblp.uni-trier.de/db/conf/sas/ sas2005.html#TerauchiA05

    2005

  33. [41]

    Amin Timany and Lars Birkedal. 2019. Mechanized relational verification of concurrent programs with continuations. Proceedings of the ACM on Programming Languages 3, ICFP (2019), 1–28

    2019

  34. [42]

    Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying Refinement and Hoare-Style Reasoning in a Logic for Higher-Order Concurrency. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (Boston, Massachusetts, USA) (ICFP ’13). Associa...

    2013

  35. [43]

    Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. 2013. Logical relations for fine-grained concurrency. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013 , Rober...

    2013

  36. [44]

    Simon Friis Vindum, Dan Frumin, and Lars Birkedal. 2022. Mechanized verification of a fine-grained concurrent queue from meta’s folly library. In CPP ’22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022 ,...

    2022

  37. [45]

    Lahiri, and William R

    Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook. 2018. Verifying equivalence of database-driven applications. Proc. ACM Program. Lang. 2, POPL (2018), 56:1–56:29. doi:10.1145/3158144

    2018 doi

  38. [46]

    Shushu Wu, Xiwei Wu, and Qinxiang Cao. 2025. EncRelTheory: EncRelTheory and Case Studies. doi:10.5281/zenodo. 16603179

    2025 doi

  39. [47]

    Xiwei Wu, Yueyang Feng, Xiaoyang Lu, Tianchuan Lin, Kan Liu, Zhiyi Wang, Shushu Wu, Lihan Xie, Chengxi Yang, Hongyi Zhong, Naijun Zhan, Zhenjiang Hu, and Qinxiang Cao. 2025. QCP: A Practical Separation Logic-based C Program Verification Tool. arXiv:2505.12878 [cs.PL] https://a...

    2025 arXiv

  40. [48]

    Hongseok Yang. 2007. Relational separation logic. Theor. Comput. Sci. 375, 1-3 (2007), 308–334. doi:10.1016/J.TCS.2006. 12.036 Encode the∀∃ Relational Hoare Logic into Standard Hoare Logic 29 A Notations The notations used in this paper are summarized in the reference table, a...

    2007 doi

  41. [51]

    Then for any terminating state 𝜎L 2 such that(𝜎L 1,𝜎 L

    |=P. Then for any terminating state 𝜎L 2 such that(𝜎L 1,𝜎 L

  42. [52]

    ∈J𝑐LKnrm, according to relational tripleJ, there exist𝜎H 2 and𝑐H 2 such that(𝜎H 1,𝑐 H

  43. [53]

    Then by Theo

    and (𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q. Then by Theo. 11, we have𝜎H 2 |= wlp(𝑐H 2,𝑋). Therefore, according to Def. 15 we derive𝜎L 2|= LQM𝑋 . • ⇐: Based on Prop. 14, for any(𝜎L 1,𝜎 H 1,𝑐 H 1)| =P, we instantiate𝑋 as the high-level terminal states set{𝜎H 3|(𝜎H 1,𝜎 H 3)∈ J𝑐H 1 Knrm}. By the ...

  44. [54]

    □ Theorem 16 (Encoded Assertion Transformation)

    and(𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q. □ Theorem 16 (Encoded Assertion Transformation). (a) L∃𝑎.P(𝑎)M𝑋 ⇐⇒ ∃𝑎. LP(𝑎)M𝑋 . (b) L𝐵∧P M𝑋 ⇐⇒ 𝐵∧ LPM𝑋 . (c) L⌊𝑃 L⌋∧P M𝑋 ⇐⇒ 𝑃 L∧ LPM𝑋 . (d) LP1∨P 2M𝑋 ⇐⇒ LP1M𝑋∨ LP2M𝑋 . Proof. (a) for any𝜎L|= L∃𝑎.P(𝑎)M𝑋 , we have∃𝑎.∃𝜎H𝑐H.(𝜎L,𝜎 H,𝑐 H)| =P∧ 𝜎H|= wlp(𝑐H...

  45. [55]

    Here(𝜎L,𝜎 H,𝑐 H 0)| =⌊𝑃 L⌋∧⌈ 𝑃 H⌉∧[ 𝑐H] is equivalent to𝜎L|=𝑃 L∧𝜎H|= 𝑃 H∧𝑐H 0 =𝑐H

    (𝜎L,𝜎 H,𝑐 H 0)| =⌊𝑃 L⌋∧⌈ 𝑃 H⌉∧ [𝑐H]∧𝜎H|= wlp(𝑐H 0,𝑋). Here(𝜎L,𝜎 H,𝑐 H 0)| =⌊𝑃 L⌋∧⌈ 𝑃 H⌉∧[ 𝑐H] is equivalent to𝜎L|=𝑃 L∧𝜎H|= 𝑃 H∧𝑐H 0 =𝑐H. Then we know𝜎L|= L⌊𝑃 L⌋∧⌈ 𝑃 H⌉∧[ 𝑐H]M𝑋 is equivalent to𝜎L|=𝑃 L∧∃𝜎H.𝜎 H|= 𝑃 H∧𝜎H|= wlp(𝑐H,𝑋). □ Corollary 21. Rule VC-FC and rule VC-Refine i...

  46. [56]

    Focus on the encoded postcondition LQ∧[ skip]M𝑋 , it is equivalent to (𝜆𝜎L 2.∃𝜎H 2 .(𝜎L 2,𝜎 H

    |= P∧𝜎H 1 |= 𝑃 H) implies the encoded precondition LP∧[𝑐H]M𝑋 . Focus on the encoded postcondition LQ∧[ skip]M𝑋 , it is equivalent to (𝜆𝜎L 2.∃𝜎H 2 .(𝜎L 2,𝜎 H

  47. [57]

    Here by definition,𝜎H 2 |= wlp(skip,𝑋) is equivalent to(𝜎H 1,𝜎 H 2)∈ J𝑐HKnrm

    |= Q∧𝜎H 2 |= wlp(skip,𝑋)). Here by definition,𝜎H 2 |= wlp(skip,𝑋) is equivalent to(𝜎H 1,𝜎 H 2)∈ J𝑐HKnrm. Then, by the triple {𝑃 H}𝑐H{𝑄H}, we know that𝜎H 2 |=𝑄H. Thus, we derive Q⊙𝑄H. • rule Enc-VC-Refine: for any𝑋 , we need to prove the triple{LP1◦ P2∧[𝑐3]M𝑋}𝑐1{LQ1◦ Q2∧[ skip]...

  48. [58]

    Then there exists 𝜎H 2 such that 𝜎H 2 |= wlp(skip,𝑋)) and 𝜎H 2 |= storePostH(𝑣)

    ∈J𝑐HKnrm, there exists 𝑣 such that 𝜎L 2 |= Exec𝑋(storePostH(𝑣),𝑐H)∧ storePostL(𝑣). Then there exists 𝜎H 2 such that 𝜎H 2 |= wlp(skip,𝑋)) and 𝜎H 2 |= storePostH(𝑣). Here by definition, 𝜎H 2 |= wlp(skip,𝑋) is equivalent to(𝜎H 1,𝜎 H 2)∈ J𝑐HKnrm. Then, by the triple {∃𝑢.𝐵 1(𝑢)∧ st...

  49. [59]

    |=P(− →𝑎) and any low-level terminal state 𝜎L 2 such that(𝜎L 1,𝜎 L

  50. [60]

    ∈𝜒(𝑓), there must exist high-level state𝜎H 2 and program𝑐H 2 such that(𝜎H 1,𝑐 H

  51. [61]

    Definition 31 (Relational Contextual Hoare Triples)

    and(𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q(− →𝑎). Definition 31 (Relational Contextual Hoare Triples). For a standard proof context Δ, a relational proof context Γ, a low-level program 𝑐L, and assertions P,Q⊆ ΣL× ΣH× ProgH, we have Δ, Γ⊢⟨P⟩ 𝑐L⟨Q⟩ if, given any environment 𝜒 such that Valid(𝜒, ...

  52. [62]

    |=P and any 𝜎L 2 such that(𝜎L 1,𝜎 L

  53. [63]

    ∈J𝑐LK𝜒 nrm, there exist 𝜎H 2 and𝑐H 2 such that (𝜎H 1,𝑐 H

  54. [64]

    C.1.3 The Encoding Theory and Call Rules

    and(𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q. C.1.3 The Encoding Theory and Call Rules. Since the relational proof contextΓ is absent in standard contextual Hoare triples, we should encode it into a standard proof context. Notice that a function specification is parameterized by a type𝐴, serving...

  55. [65]

    ∈𝜒(𝑓), there exist 𝜎H 2 and 𝑐H 2 such that(𝜎H 1,𝑐 H

  56. [66]

    Then by Theo

    and(𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q(− →𝑎). Then by Theo. 11, we have 𝜎H 2 |= wlp(𝑐H 2,𝑋). Therefore, we derive𝜎L 2|= LQ(− →𝑎)M𝑋 . • ⇐: we need to prove that for any relational function specification(𝑓 : Π(− →𝑎 :𝐴).⟨P(− →𝑎)⟩ ⟨Q(− →𝑎)⟩) in Γ, it is valid with respect to𝜒. Then given any− ...

  57. [67]

    According to Valid(𝜒, LΓM), for any 𝜎L 2 such that(𝜎L 1,𝜎 L 2)∈ 𝜒(𝑓), we have𝜎L 2|= LQ(− →𝑎)M𝑋

    ∈J𝑐H 1 Knrm} and then 𝜎L 1 |= LPM𝑋 . According to Valid(𝜒, LΓM), for any 𝜎L 2 such that(𝜎L 1,𝜎 L 2)∈ 𝜒(𝑓), we have𝜎L 2|= LQ(− →𝑎)M𝑋 . By unfolding the assertion encoding, there exist𝜎H 2 and𝑐H 2 such that𝜎H 2 |= wlp(𝑐H 2,𝑋) and(𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q(− →𝑎). According to the def...

  58. [68]

    That is for any 𝜎H 3 such that(𝜎H 2,𝜎 H 3)∈ J𝑐H 2 Knrm, we have(𝜎H 1,𝜎 H 3)∈ J𝑐H 2 Knrm

    ∈J𝑐H 2 Knrm, 𝜎H 3 |= 𝑋 . That is for any 𝜎H 3 such that(𝜎H 2,𝜎 H 3)∈ J𝑐H 2 Knrm, we have(𝜎H 1,𝜎 H 3)∈ J𝑐H 2 Knrm. Therefore, we finally derive(𝜎H 1,𝑐 H

  59. [69]

    □ Theorem 34 (Encoding Relational Contextual Triples)

    and(𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q(− →𝑎). □ Theorem 34 (Encoding Relational Contextual Triples). For any proof context Δ, Γ, low-level statement𝑐L, and assertionsP,Q⊆ ΣL× ΣH× ProgH: Δ, Γ⊢⟨P⟩ 𝑐L⟨Q⟩| {z } J iff. ∀𝑋. Δ, LΓM⊢∀{LPM𝑋}𝑐L{LQM𝑋} | {z } 𝐽 Proof. • ⇒: Given any𝜒 such thatValid(𝜒,...

  60. [70]

    Then for any terminating state 𝜎L 2 such that(𝜎L 1,𝜎 L 2)∈ J𝑐LK𝜒 nrm, according to relational tripleJ, there exist𝜎H 2 and𝑐H 2 such that (𝜎H 1,𝑐 H

    |= P. Then for any terminating state 𝜎L 2 such that(𝜎L 1,𝜎 L 2)∈ J𝑐LK𝜒 nrm, according to relational tripleJ, there exist𝜎H 2 and𝑐H 2 such that (𝜎H 1,𝑐 H

  61. [71]

    Then by Theo

    and(𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q. Then by Theo. 11, we have 𝜎H 2 |= wlp(𝑐H 2,𝑋). Therefore, according to Def. 15 we derive𝜎L 2|= LQM𝑋 . • ⇐: Given any𝜒 such that Valid(𝜒, Δ) holds and RelValid(𝜒, Γ) holds, we know Valid(𝜒, Δ) holds and Valid(𝜒, LΓM) holds. For any(𝜎L 1,𝜎 H 1,𝑐 H 1)| ...

  62. [72]

    □ Subsequently, relational Hoare logic inherits the call rule Hoare-Call in standard Hoare logic

    and(𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q. □ Subsequently, relational Hoare logic inherits the call rule Hoare-Call in standard Hoare logic. Hoare-Call 𝑓 L : Π(− →𝑎 :𝐴).{𝑃 L(− →𝑎)}{𝑄L(− →𝑎)}∈ Δ Δ⊢∀{𝑃 L(− →𝑎)} call𝑓 L{𝑄L(− →𝑎)} This rule enables provers to evaluate the call individually with a...

  63. [73]

    Due to the additional error cases in the definitions of standard and relational Hoare triples, the encoding correctness as stated in Theo

    and(𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q C.2.2 The Encoding Theory and Derived Rules. Due to the additional error cases in the definitions of standard and relational Hoare triples, the encoding correctness as stated in Theo. 4 becomes invalid and the assertion encoding L−M𝑋 needs to be adapt...

  64. [74]

    Then by Theo

    |=Q. Then by Theo. 11, we have 𝜎H 2 |= wlp(𝑐H 2,𝑋). Therefore, accord- ing to Def. 15 we derive𝜎L 2|= LQM𝑋 . • ⇐: For any(𝜎L 1,𝜎 H 1,𝑐 H

  65. [75]

    Then, we prove two cases: – error simulation: when𝜎L 1∈ J𝑐LKerr, then𝜎H 1 ∈ J𝑐H 1 Kerr, then this case proved

    inP, we instantiate𝑋 as{𝜎H 3 |( 𝜎H 1,𝜎 H 3)∈ J𝑐H 1 Knrm}, and observe that if𝜎H 1 ∉ J𝑐H 1 Kerr then𝑐H 1 ∈ LPM𝑋 . Then, we prove two cases: – error simulation: when𝜎L 1∈ J𝑐LKerr, then𝜎H 1 ∈ J𝑐H 1 Kerr, then this case proved. Otherwise, 𝜎H 1 ∉ J𝑐H 1 Kerr. Then𝜎L 1∈ LPM𝑋 and from...

  66. [76]

    Therefore, we get(𝜎H 1,𝑐 H

    ∈J𝑐H 2 Knrm,𝜎H 3 ∈ {𝜎H 0 |( 𝜎H 1,𝜎 H 0)∈ J𝑐H 2 Knrm}, and𝜎H 2 ∉ J𝑐H 2 Kerr. Therefore, we get(𝜎H 1,𝑐 H

  67. [77]

    ↩→( 𝜎H 2,𝑐 H 2). □ 38 Shushu Wu, Xiwei Wu, and Qinxiang Cao / / {Exec𝑋(AH =𝑙,sH ={} ; jH = 0; while jH < 8 do...)∧ AL =𝑙} / / consequence rules / / {Exec𝑋(sH =∅∧ jH = 0∧ AH =𝑙,while jH < 8 do...)∧ AL =𝑙} xL = 0; iL = 0; / / sequencing rules / / {∃𝑙0𝑛. Exec𝑋(sH =𝑙0∧ jH =𝑛∧ AH =...

  68. [79]

    C.3.2 The Encoding Theory

    and(𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q. C.3.2 The Encoding Theory. According to separation logic, the environment untouched by the high-level program should be preserved. Consequently, we can augment the placeholder𝑋⊆ ΣH with a framing assertion 𝐹 H⊆ ΣH, representing unchanged states durin...

  69. [80]

    Then for any terminating state 𝜎L 2 such that (𝜎L 1,𝜎 L 2)∈ J𝑐LKnrm, according to relational tripleJ, there exist𝜎H 2 and𝑐H 2 such that(𝜎H 1 ∪· 𝜎H 𝑓 ,𝑐 H

    |=P. Then for any terminating state 𝜎L 2 such that (𝜎L 1,𝜎 L 2)∈ J𝑐LKnrm, according to relational tripleJ, there exist𝜎H 2 and𝑐H 2 such that(𝜎H 1 ∪· 𝜎H 𝑓 ,𝑐 H

  70. [81]

    ↩→( 𝜎H 2 ∪·𝜎H 𝑓 ,𝑐 H

  71. [82]

    Then by Theo

    and(𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q. Then by Theo. 11, we have 𝜎H 2 ∪·𝜎H 𝑓 |= wlp(𝑐H 2,𝑋). Therefore, according to Def. 15 we derive𝜎L 2|= LQM𝑋 . • ⇐: Based on Prop. 14, for any environment 𝜎H 𝑓 , any(𝜎L 1,𝜎 H 1,𝑐 H 1)| =P, we instantiate 𝑋 as the high-level terminal states set{𝜎H 3|(𝜎H...

  72. [83]

    By unfolding the assertion encoding, there exist𝜎H 2 and𝑐H 2 such that𝜎H 2 ∪·𝜎H 𝑓 |= wlp(𝑐H 2,𝑋) and(𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q

    ∈J𝑐LKnrm, we have 𝜎L 2 |= LQM𝑋 . By unfolding the assertion encoding, there exist𝜎H 2 and𝑐H 2 such that𝜎H 2 ∪·𝜎H 𝑓 |= wlp(𝑐H 2,𝑋) and(𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q. According to the definition of weakest preconditions, for any𝜎H 3 such 40 Shushu Wu, Xiwei Wu, and Qinxiang Cao that(𝜎H ...

  73. [84]

    □ D Examples Here we list the examples used in this paper and provide both relational and standard proofs for them

    ↩→( 𝜎H 2∪·𝜎H 𝑓 ,𝑐 H 2) and(𝜎L 2,𝜎 H 2,𝑐 H 2)| =Q. □ D Examples Here we list the examples used in this paper and provide both relational and standard proofs for them. Example 1. The low-level program (on the left) assigns the variable x to either 0 or 1. In contrast, the high-l...

  74. [2021]

    In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (Virtual, Canada) (PLDI 2021)

    Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (Virtual, Canada) (PLDI 2021). Association for Computing Machinery, New York, ...

    2021

  75. [2023]

    An Algebra of Alignment for Relational Verification. Proc. ACM Program. Lang. 7, POPL (2023), 573–603. doi:10.1145/3571213

    2023 doi

Pith tools

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