Pith. sign in

REVIEW 2 major objections 5 minor 1 cited by

Forall-Exists Relational Verification by Filtering to Forall-Forall

T0 review · 2 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read By instrumenting a paired product program with filtering assertions, this paper proves that a forall-forall verification success implies the original forall-exists relational specification.

desk verdict A genuinely useful reduction of forall-exists to forall-forall, with a real but likely repairable gap in the printed proof of the key lemma. read the letter →

arxiv 2509.04777 v1 pith:BK2YW5VN submitted 2025-09-05 cs.LO cs.PL

Ramana Nagasamudram , Anindya Banerjee , David A. Naumann This is my paper · ORCID
classification cs.LOcs.PL MSC 68N3003B7068Q60
keywords relationalverificationforall-existspropertiesproductprogramsbicomsfilter-adequacytransformationnondeterminismauto-activeprogramlogic
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 tries to establish a route from hard relational program properties to easy ones: any $\forall\exists$ correctness judgment between two nondeterministic programs can be verified by building a paired product program, instrumenting it with filtering assertions, and then proving an ordinary $\forall\forall$ property of the instrumented product. The central soundness theorem says that if the transformed product satisfies its specification, the original pair of programs really does satisfy the $\forall\exists$ judgment. This matters because $\forall\forall$ verification is well supported by existing logics and tools, while $\forall\exists$ verification---needed for nondeterminism, refinement, and generalized noninterference---has few practical tools. The paper backs the claim with a program logic, a fully mechanized proof, and a working prototype that verifies the paper's examples through an existing SMT-based verifier.

What carries the argument

The load-bearing object is the bicom, a syntactic product program that runs a pair of commands side by side with explicit alignment constructs: the embed $\langle c|c'\rangle$, bi-if, bi-while with data-dependent alignment conditions, and the havoc-filter $\mathit{havf}_x\,Q$, which nondeterministically picks a right-side value for $x$ and then assumes the relation $Q$. The filter-adequacy transformation $\mathit{chk}$ instruments each loop with snapshot variables and asserts that the declared variant decreases on right-only iterations, and guards every havoc-filter with an existential assertion ensuring that a witness value exists. These inserted assertions are what turn $\forall\exists$ adequacy into a $\forall\forall$ verification condition; the semantic framing condition $\mathit{bFrame}(B,\mathit{vs})$ keeps the instrumentation from interfering with the underlying executions.

What would settle it

Search for a well-formed bicom $B$ and relations $R,S$ such that $B$ is framed by $\mathit{vs}$, $\mathit{vs}$ frames $R$ and $S$, and $\models \mathit{chk}(B,\mathit{vs}) : R\ \yen\ S$ holds while $\models \mathit{left}(B)|\mathit{right}(B) : R\ \exists{\approx\!\!>}\ S$ fails; the theorem says no such instance exists, so a small brute-force enumeration over finite-state commands would settle the claim. A more operational check: use the prototype on a pair where the bicom's projection is not equivalent to the intended program, e.g., $\langle x:=0|\mathit{skip}\rangle;\mathit{havf}_y(y=0)$ for $\mathit{hav}\,x\,|\,\mathit{hav}\,y$ with postcondition $x=0$; if the tool reports success, it is not enforcing the representation condition.

Watch

Extended reading notes

Core claim

The paper's central claim is Theorem 5.4: from a well-formed bicom $B$ framed by a variable list $\mathit{vs}$, if the instrumented bicom $\mathit{chk}(B,\mathit{vs})$ is correct for pre-relation $R$ and post-relation $S$ in the $\forall\forall$ sense, then the left and right projections of $B$ satisfy the $\forall\exists$ judgment $R\ \exists{\approx\!\!>}\ S$. In other words, the filter-adequacy transformation turns the existence of a matching right-side execution into a checkable universal property of a product program, provided the original programs are semantically equivalent to the projections of $B$ and the framing conditions hold. The proof works by deriving, from the weakest-precondition equations of the instrumented bicom, exactly the premises of the paper's program-logic rules for the projections.

Load-bearing premise

The method only works if the user's product program actually represents the two programs being verified: the bicom's left and right projections must be equivalent to the two unary programs, and the supplied framing list must cover every variable the programs and specifications depend on; the paper's prototype checks these conditions manually rather than automatically.

Editorial extensions

If this is right

  • A successful forall-forall verification of the transformed bicom is sufficient evidence for the forall-exists specification of the actual programs, so users can work with ordinary assertions and standard verifiers.
  • Right-side divergence, the main obstacle in forall-exists reasoning, is handled by filtering right-side executions to those that decrease the declared variant, making may-termination a by-product of the forall-forall check.
  • Data-dependent loop alignments, not just lockstep or fixed n,m alignments, are supported, which covers stuttering loops and conditional alignments such as the paper's running example.
  • The soundness theorem is independent of how the forall-forall property is discharged, so the same transformation can be used with any verification technique, including testing.
  • The theory is proved for a small core language, but the structure of the proof is designed to adapt to richer programming languages and assertion languages.

Reading between the lines

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

  • The same filter-adequacy idea could plausibly extend to forall-exists properties with multiple existential witnesses, since existing k-safety product encodings could be instrumented in the same way.
  • Because the transformation is purely syntactic and linear-time, one could automate the search over candidate bicoms: generate alignments, apply chk, and let an SMT solver decide the forall-forall check, turning the methodology into a fully automatic procedure for decidable fragments.
  • The paper's reliance on user-supplied framing lists and manual projection checks suggests that the next practical step is to infer frames automatically and discharge projection equivalence with a syntax-directed checker; if those checks are automated, the method becomes a drop-in front-end for existing auto-active verifiers.
  • The treatment of right-side may-termination via filtering could also serve as a lightweight termination argument in settings where must-termination is too strong, such as probabilistic program refinement with almost-sure termination.
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 / 5 minor

Summary. The paper proposes a method to verify ∀∃ (forall-exists) relational properties of nondeterministic imperative programs by reducing them to ∀∀ (forall-forall) properties of a transformed product program, called a bicom. It introduces ERHL, a program logic for ∀∃ judgments extended with assertion failures; defines bicoms with a big-step semantics, weakest preconditions, and framing conditions; and defines a filter-adequacy transformation chk that adds assertions to a bicom so that successful ∀∀ verification of chk(B) implies the desired ∀∃ property for the projections of B. The main result is Theorem 5.4. A prototype based on Why3 is described and used to verify several examples, and the paper claims full mechanization in Rocq.

Significance. If the main theorem is correct, this is a significant contribution: it offers a way to leverage mature auto-active verification tools for ∀∃ properties, which are notoriously harder than ∀∀ properties. The paper is well structured, provides detailed semantic definitions, and includes an extended appendix with proofs. The authors also give explicit credit to the sources of their proof rules and discuss related work thoroughly. The claimed Rocq mechanization, if made available, would strengthen confidence considerably, but in the absence of a public artifact the correctness of the central theorem rests on the written proofs, which contain a serious gap (see Major Comment 1).

major comments (2)
  1. [Appendix A, proof of Lemma 5.3, while case] The invariant is defined as I := wlpR(x:=e_v; uchk(d); assert(0≤e_v<x), S), the wlp of a single loop body. However, the assumption |= ⟨skip|uchk(while e vnt e_v do d)⟩ : R ¥{S gives, via wlp/correctness, R⇒wlpR(uchk(while...), S), which by the loop equation is R⇒gfp(F) for the function F of Lemma 4.9. The step 'so by definition of wlpR and wlp/correctness lemma we have |= R⇒I' is therefore not a logical consequence, since gfp(F) does not imply wlpR(body, S) in general. For example, take c = while false do skip with e_v = 0 and S = true; then wlpR(uchk(c), S) = true while wlpR(body, S) = false, so the claimed implication fails. The proof appears repairable by defining I as wlpR(uchk(while...), S) (the greatest fixpoint), which makes R⇒I immediate and still allows the derivation of the eSkipDo premise from the post-fixpoint property, but as printed the proof is invalid. Since the embed case of Theorem 5.4 appeals to Lemma 5.3, this gap directly affects the central soundness claim.
  2. [Section 1 and Appendix A] The paper states that 'The theorem has also been fully mechanized in Rocq' and that missing details can be found in the Rocq development, but no artifact, repository, or link is provided. Given the subtlety of the proofs—exemplified by the gap in Lemma 5.3—an independent check of the mechanization is essential to validate the central claim. Without the artifact, the claimed machine-checked proof cannot be confirmed, and the written proof alone is insufficient.
minor comments (5)
  1. [Abstract] The abstract contains a spelling error: 'specificaton' should be 'specification'; the authors may also want to proofread the phrase 'the the existentially quantified asserts' in Section 6.
  2. [Lemma 4.7] The label 'adeqacy' is misspelled; it should be 'adequacy'.
  3. [Section 3, footnote 3] The derivation of eSkipIf refers to 'rIf' but no rule with that name appears in the paper; the intended rule is likely eIf4 or eRewrite. Please clarify the reference.
  4. [Section 6] The statement that checking conditions ↼−B≃c and −⇀B≃c′ 'was done manually for our examples' is a significant limitation of the methodology; it deserves more prominence, since a mistake in this step would make the verified ∀∀ property irrelevant to the original programs.
  5. [Appendix A, Theorem 5.4, loop case] The notation −⇀ ⇀ for the bi-right projection is difficult to parse in the calculation; consider introducing a more mnemonic name or a brief explanation of its use in that proof.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Theorem 5.4 is proved from the bicom semantics and wlp equations; self-citations are background, not load-bearing.

full rationale

The central claim, Theorem 5.4, is not circular. It derives a forall-exists judgment for the projections from a forall-forall correctness judgment of the chk-transformed bicom, using the wlp equations of Lemma 4.10, the framing results of Lemmas 4.13–4.15, and the soundness of the ERHL proof rules (Theorem 3.3), all of which are proved in the paper or appendix. The ERHL rules are adapted from the authors' own preprint [52], but Theorem 3.3 re-proves their soundness in this paper, so the self-citation is not load-bearing. The word 'filtered' is borrowed from [52], but the filter-adequacy transformation itself is defined in Figures 11–12 and its soundness is proved here, so borrowing the term does not reduce the derivation to an input. No equation appears to be equivalent to its own conclusion by construction: for instance, the havf base case reduces the transformed bicom's correctness to R ⇒ ∃|x.S, and then uses rule eSkipHav to obtain skip|hav x : R ∃≈> S; the derived judgment is genuinely different from the assumed one. A proof-correctness caveat exists: in the printed while case of Lemma 5.3, the chosen invariant is wlp of one loop body and the step claiming it is a post-fixpoint of the loop equation may not hold as written, and the claimed Rocq mechanization is not released. These are soundness/artifact concerns, not circularity, and per the rubric they are excluded from the circularity score.

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

The central claim rests on standard mathematical axioms and on domain assumptions about the imperative language and product semantics. There are no numeric free parameters or fitted values. The only invented constructs (bicoms, havf, chk) are definitions inside the paper, not independent postulates.

assumptions (5)
  • standard math Classical logic, functional extensionality, and propositional extensionality are available in the ambient logic (Rocq).
    Section 3 states the mechanization uses the Classical, FunctionalExtensionality, and PropExtensionality libraries; these are standard but not constructive.
  • domain assumption Assertions and relations are shallow embedded as sets in the ambient set theory; expressions are total functions from stores.
    Section 3.1; this avoids expressiveness issues and lets wlp be defined in the ambient logic, but it means the results are not tied to a concrete assertion syntax.
  • domain assumption Nondeterminism is represented only by havoc statements; programs are type-correct and operate on denumerable integer and boolean variables.
    Section 3.1 and Section 7; the core theorem is for this simple language, not for procedures, pointers, or other nondeterminism sources.
  • standard math Fresh snapshot variables can always be chosen outside the frame list and outside modified variables of instrumented subterms; in the mechanization this is via Hilbert's indefinite choice.
    Section 5.1; the transformation is parameterized by an avoid list and relies on existence of such variables, which holds because the variable sets are denumerable.
  • domain assumption The bi-while semantics bakes in an adequacy condition and determinizes the choice between left-only and right-only iterations; failure may be masked by one-sided divergence.
    Section 4.2, Figure 9; this choice is needed for translation to ordinary commands and for the main theorem, but it is a modeling assumption about product semantics.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Forall-Exists Relational Verification by Filtering to Forall-Forall." pith.science (2026). https://pith.science/paper/BK2YW5VN

@misc{pith2026250904777,
  author       = {Pith},
  title        = {Pith review of: Forall-Exists Relational Verification by Filtering to Forall-Forall},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BK2YW5VN}},
  note         = {Machine review of arXiv:2509.04777}
}
abstract

Relational verification encompasses research directions such as reasoning about data abstraction, reasoning about security and privacy, secure compilation, and functional specificaton of tensor programs, among others. Several relational Hoare logics exist, with accompanying tool support for compositional reasoning of $\forall\forall$ (2-safety) properties and, generally, k-safety properties of product programs. In contrast, few logics and tools exist for reasoning about $\forall\exists$ properties which are critical in the context of nondeterminism. This paper's primary contribution is a methodology for verifying a $\forall\exists$ judgment by way of a novel filter-adequacy transformation. This transformation adds assertions to a product program in such a way that the desired $\forall\exists$ property (of a pair of underlying unary programs) is implied by a $\forall\forall$ property of the transformed product. The paper develops a program logic for the basic $\forall\exists$ judgement extended with assertion failures; develops bicoms, a form of product programs that represents pairs of executions and that caters for direct translation of $\forall\forall$ properties to unary correctness; proves (using the logic) a soundness theorem that says successful $\forall\forall$ verification of a transformed bicom implies the $\forall\exists$ spec for its underlying unary commands; and implements a proof of principle prototype for auto-active relational verification which has been used to verify all examples in the paper. The methodology thereby enables a user to work with ordinary assertions and assumptions, and a standard assertion language, so that existing tools including auto-active verifiers can be used.

Figures

Figures reproduced from arXiv: 2509.04777 by the authors.

Figure 1
Figure 1. Program 𝑐1 and a bicom for two copies of𝑐1. Notation such as ⌊ z := 0 ⌋ denotes bicom ⟨𝑧 := 0 | 𝑧 := 0⟩. Notation ⟨[𝑤 ≠ 0⟨] means 𝑤 ≠ 0 in the left state; [⟩𝑤 ≠ 0]⟩ means 𝑤 ≠ 0 in the right state. What should the elided assumption be? If we use 𝑥 =¥ 𝑦, the assertion added by chk will be as before, and will not fail. But that assumption does not support successful verification of true {¥ 𝑥 =¥ 𝑦 because of course from… view at source ↗
Figure 2
Figure 2. The chk function applied to the bicom in Figure [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Bicoms 𝐵1. . .𝐵4 capture different alignments of 𝑐2 | 𝑐2. Summary. The filter-adequacy transformation supports the following methodology for verifying a ∀∃ judgment 𝑐 | 𝑐 ′ : R ∃ ≈> S. (1) Find a bicom 𝐵 that represents 𝑐, 𝑐′ in the sense that it’s projections are semantically equivalent to 𝑐 and 𝑐 ′ . Moreover 𝐵 should represent a helpful alignment in which right-side havocs are accompanied by filter assumptions, a… view at source ↗
Figures from the paper (10 more)
Figure 4
Figure 4. Figure 4: Semantics of selected commands. The outcome [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]
Figure 5
Figure 5. Figure 5: ERHL: Core rules for the ∃ ≈> judgment eSkipDo skip | 𝑐 : [⟩𝑒 ]⟩ ∧ R ∧ (𝑛 = 𝐸) ∃ ≈> Q ∧ (0 ≤ 𝐸 < 𝑛) for all 𝑛 ∈ Z skip | while 𝑒 do 𝑐 : Q ∃ ≈> Q ∧ ¬[⟩𝑒 ]⟩ eSkipIf skip | 𝑐 : [⟩𝑒 ]⟩ ∧ R ∃ ≈> S skip | 𝑑 : ¬[⟩𝑒 ]⟩ ∧ R ∃ ≈> S skip | if 𝑒 then 𝑐 else 𝑑 : R ∃ ≈> S [PITH_FUL…
Figure 6
Figure 6. Figure 6: Derived rules for ∃ ≈> [PITH_FULL_IMAGE:figures/full_fig_p010_6.png]
Figure 7
Figure 7. Figure 7: Left (↼− 𝐵 ) and right (⇀− 𝐵 ) syntactic projections of bicoms 𝐵. −−−−⇀⇀ ⟨𝑐 | 𝑐 ′ ⟩ = ⟨skip | 𝑐 ′ ⟩ −−−−−−⇀⇀ assert P = assert P −−−−−−−⇀⇀ havf 𝑥 R = havf 𝑥 R −−−−⇀⇀ 𝐵1; 𝐵2 = ⇀⇀− 𝐵1 ; ⇀⇀− 𝐵2 −−−−−−−−−−−−−−−⇀⇀ if 𝑒 |𝑒 ′ 𝐵1 𝐵2 𝐵3 𝐵4 = if tt|𝑒 ′ ⇀⇀− 𝐵1 ⇀⇀− 𝐵2 ⇀⇀− 𝐵3 ⇀⇀− 𝐵…
Figure 9
Figure 9. Figure 9: Bicom semantics. Here 𝑊 abbreviates while 𝑒 |𝑒 ′ algn L|R do 𝐵. Connections with stronger relations used in other works [2, 24] are discussed in Section 7. Here we are not concerned with the rewriting of bicoms in general, but only eliminating skips introduced by the p…
Figure 10
Figure 10. Figure 10: Defining cFrame and bFrame. Here 𝑣𝑠 ⊩ (𝑒, 𝑒′ , . . .) abbreviates 𝑣𝑠 ⊩ 𝑒 ∧ 𝑣𝑠 ⊩ 𝑒 ′ ∧ . . .. Lemma 4.15. If bFrame(𝐵, 𝑣𝑠) and 𝑥 ∉ 𝑣𝑠 then, for any 𝑛 ∈ Z, |= (wlp(𝐵, R))|𝑥 |𝑛 ⇒ wlp(𝐵, R |𝑥 |𝑛 ). We conclude the section with straightforward results involving substitutio…
Figure 11
Figure 11. Figure 11: The uchk transformation on commands a set of variables to avoid, which should be chosen to frame the spec and bicom of interest. For simplicity the set is represented by a list. The unary check function maps a command 𝑐 and list𝑣𝑠 of variables to a command uchk(𝑐, 𝑣𝑠)…
Figure 12
Figure 12. Figure 12: The chk transformation on bicoms In the loop case, the two-state expression 𝐸 is used as a variant. It is only relevant for right-only iterations where it must decrease (due to changes on the right side since any left variables will remain unchanged). Integer variable…
Figure 13
Figure 13. Figure 13: Size of commands and bicoms 𝑠 |= 𝑝 assert 𝑝/𝑠 ⇓ 𝑠 𝑠 ̸|= 𝑝 assert 𝑝/𝑠 ⇓ 𝑛 ∈ Z hav 𝑥/𝑠 ⇓ 𝑠[𝑥 ↦→ 𝑛] 𝑠(𝑒) = 𝑛 𝑥 := 𝑒/𝑠 ⇓ 𝑠[𝑥 ↦→ 𝑛] 𝑐/𝑠 ⇓ 𝑡 𝑑/𝑡 ⇓ 𝜙 𝑐;𝑑/𝑠 ⇓ 𝜙 𝑐/𝑠 ⇓ 𝑐;𝑑/𝑠 ⇓ 𝑠 |= 𝑒 𝑐/𝑠 ⇓ 𝜙 if 𝑒 then 𝑐 else 𝑑/𝑠 ⇓ 𝜙 𝑠 ̸|= 𝑒 𝑑/𝑠 ⇓ 𝜙 if 𝑒 then 𝑐 else 𝑑/𝑠 ⇓ 𝜙 𝑠 ̸|= 𝑒 while 𝑒 do 𝑐…
Figure 14
Figure 14. Figure 14: Semantics of commands Remark A.1. Definition 4.3 of  does not include congruence clauses. It may seem natural to include them even though we have no specific use for them. In fact congruence with respect to sequence and bi-if is no problem, but congruence for bi-whil…

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

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

  1. Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI

    cs.AI 2026-08 conditional novelty 5.0 of 10

    A corrected, machine-checked proof shows that relational safety implies epistemic security for reactive programs with declassification annotations.

Reference graph

Works this paper leans on

61 extracted references · 21 canonical work pages · cited by 1 Pith paper

  1. [1]

    Carmine Abate, Roberto Blanco, Ştefan Ciobâcă, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, and Jérémy Thibault. 2021. An Extended Account of Trace-relating Compiler Correctness and Secure Compilation.ACM Trans. Program. Lang. Syst.43, 4 (2021), 14:1–14:48. https://doi.org/10.1145/3460860

    doi:10.1145/3460860 2021

  2. [2]

    Naumann, and Minh Ngo

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

    work page

  3. [3]

    Apt, Frank S

    Krzysztof R. Apt, Frank S. de Boer, and Ernst-Rüdiger Olderog. 2009.Verification of Sequential and Concurrent Programs (3 ed.). Springer. https://doi.org/10.1007/978-1-84882-745-5

    doi:10.1007/978-1-84882-745-5 2009

  4. [4]

    Flavio Ascari, Roberto Bruni, Roberta Gori, and Francesco Logozzo. 2024. Sufficient Incorrectness Logic: SIL and Separation SIL. arXiv:2310.18156 [cs.LO]

    arXiv 2024

  5. [5]

    Martin Avanzini, Gilles Barthe, Davide Davoli, and Benjamin Grégoire. 2025. A Quantitative Probabilistic Relational Hoare Logic.Proc. ACM Program. Lang.9, POPL (2025). https://doi.org/10.1145/3704876

    doi:10.1145/3704876 2025

  6. [6]

    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 Transactions on Programming Languages and Systems44, 4 (2022), 25:1–25:136. https://doi.org/10.1145/3551497

    work page doi:10.1145/3551497 2022

  7. [7]

    Naumann, and Mohammad Nikouei

    Anindya Banerjee, David A. Naumann, and Mohammad Nikouei. 2016. Relational Logic with Framing and Hypotheses. InFoundations of Software Tech. and Theoretical Comp. Sci.11:1–11:16. Technical report at http://arxiv.org/abs/1611. 08992

    work page 2016

  8. [8]

    Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2016. Product Programs and Relational Program Logics.J. Logical and Algebraic Methods in Programming85, 5 (2016), 847–859

    work page 2016

Show all 61 references
  1. [9]

    D’Argenio, and Tamara Rezk

    Gilles Barthe, Pedro R. D’Argenio, and Tamara Rezk. 2011. Secure information flow by self-composition.Math. Struct. Comput. Sci.21, 6 (2011), 1207–1252. https://doi.org/10.1017/S0960129511000193

    2011 doi

  2. [10]

    Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, and Matteo Maffei. 2019. Verifying Relational Properties using Trace Logic. InFormal Methods in Computer Aided Design (FMCAD). https://doi.org/10. 23919/FMCAD.2019.8894277

    2019

  3. [11]

    Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2017. Coupling proofs are probabilistic product programs. InACM Symposium on Principles of Programming Languages. 161–174. https://doi.org/10.1145/3009837. 3009896

    2017 doi

  4. [12]

    Gilles Barthe and Tamara Rezk. 2005. Non-interference for a JVM-like language. InProceedings of TLDI’05

    2005

  5. [13]

    N. Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. InACM Symposium on Principles of Programming Languages. ACM, 14–25. https://doi.org/10.1145/964001.964003

    2004

  6. [14]

    Lennart Beringer. 2011. Relational Decomposition. InInteractive Theorem Proving (LNCS), Vol. 6898. 39–54. https: //doi.org/10.1007/978-3-642-22863-6_6

    2011 doi

  7. [17]

    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.Journal of Automated Reasoning61, 1 (2018), 367–422. https: //doi.org/10.1007/s10817-018-9457-5

    2018 doi

  8. [18]

    Churchill, Oded Padon, Rahul Sharma, and Alex Aiken

    Berkeley R. Churchill, Oded Padon, Rahul Sharma, and Alex Aiken. 2019. Semantic program alignment for equivalence checking. InACM Conf. on Program. Lang. Design and Implementation. 1027–1040. https://doi.org/10.1145/3314221. 3314596

    2019 doi

  9. [19]

    Cohen and Philip Johnson-Freyd

    Joshua M. Cohen and Philip Johnson-Freyd. 2024. A Formalization of Core Why3 in Coq.Proc. ACM Program. Lang.8, POPL, Article 60 (Jan. 2024), 30 pages. https://doi.org/10.1145/3632902

    2024 doi

  10. [20]

    Arthur Correnson, Tobias Nießen, Bernd Finkbeiner, and Georg Weissenbacher. 2024. Finding∀∃ Hyperbugs using Symbolic Execution.Proc. ACM Program. Lang.8, OOPSLA2 (2024), 1420–1445. https://doi.org/10.1145/3689761

    2024 doi

  11. [21]

    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. https://doi.org/10.1145/3689756

    2024 doi

  12. [22]

    Thibault Dardinier and Peter Müller. 2024. Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties.Proc. ACM Program. Lang.8, PLDI (2024), 1485–1509. https://doi.org/10.1145/3656437

    2024 doi

  13. [23]

    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 (2025). https://doi.org/10.1145/3704856 38 Ramana Nagasamudram, ...

    2025 doi

  14. [24]

    Robert Dickerson, Prasita Mukherjee, and Benjamin Delaware. 2025. KestRel: Relational Verification using E-Graphs for Program Alignment.Proc. ACM Program. Lang.9, OOPSLA1 (2025), 1073–1100. https://doi.org/10.1145/3720474

    2025 doi

  15. [25]

    Zhang, and Benjamin Delaware

    Robert Dickerson, Qianchuan Ye, Michael K. Zhang, and Benjamin Delaware. 2022. RHLE: Modular Deductive Verification of Relational∀∃ Properties. InAsian Symposium on Programming Languages and Systems (LNCS), Vol. 13658. 67–87. https://doi.org/10.1007/978-3-031-21037-2_4

    2022 doi

  16. [26]

    Dijkstra

    Edsger W. Dijkstra. 1976.A Discipline of Programming. Prentice-Hall

    1976

  17. [27]

    Dijkstra and Carel S

    Edsger W. Dijkstra and Carel S. Scholten. 1990.Predicate Calculus and Program Semantics. Springer. https://doi.org/ 10.1007/978-1-4612-3228-5

    1990 doi

  18. [28]

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

    2022 doi

  19. [29]

    Marco Eilers, Thibault Dardinier, and Peter Müller. 2023. CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity.Proc. ACM Program. Lang.7, PLDI (2023). https://doi.org/10.1145/3591289

    2023 doi

  20. [30]

    Jean-Christophe Filliâtre and Andrei Paskevich. 2013. Why3 — Where Programs Meet Provers. InProgramming Languages and Systems

    2013

  21. [31]

    Robert Floyd. 1967. Assigning Meaning to Programs. InSymp. on Applied Math. 19, Math. Aspects of Comp. Sci.Amer. Math. Soc., 19–32

    1967

  22. [32]

    Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2018. ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. InIEEE Symp. on Logic in Computer Science. 442–451. https://doi.org/10.1145/3209108.3209174

    2018

  23. [33]

    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). https://doi.org/10.114...

    2022 doi

  24. [34]

    Amarasinghe, and Ilya Sergey

    Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman P. Amarasinghe, and Ilya Sergey. 2024. Mechanised Hypersafety Proofs about Structured Data.Proc. ACM Program. Lang.8, PLDI (2024), 647–670. https://doi.org/10. 1145/3656403

    2024

  25. [35]

    Leandro Gomes, Patrick Baillot, and Marco Gaboardi. 2025. BiGKAT: An Algebraic Framework for Relational Verification of Probabilistic Programs. InFoundations of Software Science and Computation Structures, Parosh Aziz Abdulla and Delia Kesner (Eds.). https://doi.org/10.1007/97...

    2025 doi

  26. [36]

    Michael Greenberg, Ryan Beckett, and Eric Hayden Campbell. 2022. Kleene algebra modulo theories: a framework for concrete KATs. InACM Conf. on Program. Lang. Design and Implementation. https://doi.org/10.1145/3519939.3523722

    2022

  27. [37]

    Haselwarter, Joseph Tassarotti, and Lars Birkedal

    Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. 2024. Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.Proc. ACM Program. Lang.8, POPL (2024). https://doi.org/10.1145/3632868

    2024 doi

  28. [38]

    Arie Gurfinkel. 2022. Program Verification with Constrained Horn Clauses (Invited Paper). InComputer Aided Verification, Sharon Shoham and Yakir Vizel (Eds.). https://doi.org/10.1007/978-3-031-13185-1_2

    2022 doi

  29. [40]

    C. A. R. Hoare. 1978. Some Properties of Predicate Transformers.J. ACM25 (1978), 461–480

    1978

  30. [41]

    Shachar Itzhaky, Sharon Shoham, and Yakir Vizel. 2024. Hyperproperty Verification as CHC Satisfiability. InPro- gramming Languages and Systems, European Symposium on Programming (LNCS), Vol. 14577. 212–241. https: //doi.org/10.1007/978-3-031-57267-8_9

    2024 doi

  31. [42]

    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. https://doi.org/10.1017/S0956796818000151

    2018 doi

  32. [43]

    Dexter Kozen. 1997. Kleene algebra with tests.ACM Transactions on Programming Languages and Systems19, 3 (1997), 427–443. https://doi.org/10.1145/256167.256195

    1997

  33. [44]

    Dexter Kozen and Frederick Smith. 1996. Kleene algebra with tests: Completeness and decidability. InInternational Workshop on Computer Science Logic (LNCS), Vol. 1258. 244–259. https://doi.org/10.1007/3-540-63172-0_43

    1996 doi

  34. [45]

    Schneider

    Leslie Lamport and Fred B. Schneider. 2021. Verifying Hyperproperties With TLA. InIEEE Computer Security Foundations. 1–16. https://doi.org/10.1109/CSF51468.2021.00012

    2021

  35. [46]

    Rustan M

    K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. InLogic for Programming, Artificial Intelligence, and Reasoning, Edmund M. Clarke and Andrei Voronkov (Eds.). https://doi.org/10.1007/978-3- 642-17511-4_20

    2010 doi

  36. [47]

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

    2020 doi

  37. [48]

    Konstantinos Mamouras. 2017. Equational Theories of Abnormal Termination Based on Kleene Algebra. InFoSSaCS. 88–105. Forall-Exists Relational Verification by Filtering to Forall-Forall[with appendix]39

    2017

  38. [49]

    Peter Müller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission- Based Reasoning. InInt’l Conf. on Verification, Model Checking, and Abstract Interpretation. https://doi.org/10.1007/978- 3-662-49122-5_2

    2016 doi

  39. [50]

    Nagasamudram, A

    R. Nagasamudram, A. Banerjee, and D.A. Naumann. 2025. WhyRel: an auto-active relational verifier.International Journal on Software Tools for Technology Transfer(2025). https://doi.org/10.1007/s10009-025-00786-1

    2025 doi

  40. [52]

    Ramana Nagasamudram, Anindya Banerjee, and David A. Naumann. 2025. Alignment complete relational Hoare logics for some and all.CoRRabs/2307.10045 (2025). https://doi.org/10.48550/arXiv.2307.10045

    2025 doi

  41. [53]

    1992.Semantics with Applications - a Formal Introduction

    Hanne Riis Nielson and Flemming Nielson. 1992.Semantics with Applications - a Formal Introduction. Wiley, New York

    1992

  42. [54]

    Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey

    Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey. 2024.Programming Language Foundations. Software Foundations, Vol. 2. Version 6.7, http://softwarefoundations.ci...

    2024

  43. [55]

    Ron Shemer, Arie Gurfinkel, Sharon Shoham, and Yakir Vizel. 2019. Property Directed Self Composition. InComputer Aided Verification (LNCS), Vol. 11561. 161–179. https://doi.org/10.1007/978-3-030-25540-4_9

    2019 doi

  44. [56]

    Marcelo Sousa and Isil Dillig. 2016. Cartesian Hoare logic for verifying k-safety properties. InACM Conf. on Program. Lang. Design and Implementation. 57–69. https://doi.org/10.1145/2908080.2908092

    2016

  45. [57]

    Ofer Strichman and Maor Veitsman. 2016. Regression Verification for Unbalanced Recursive Functions. InFM 2016: Formal Methods. 645–658

    2016

  46. [58]

    Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. InACM SIGPLAN International Conference on Functional Programming. https://doi.org/10. 1145/2500365.2500600

    2013

  47. [59]

    Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. 2021. Constraint-Based Relational Verification. InComputer Aided Verification (LNCS), Vol. 12759. 742–766. https://doi.org/10.1007/978-3-030-81685-8_35

    2021 doi

  48. [60]

    Zhongye Wang, Qinxiang Cao, and Yichen Tao. 2024. Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding.J. Autom. Reason.68, 3 (2024), 18. https://doi.org/10.1007/S10817-024-09706-5

    2024 doi

  49. [61]

    Shushu Wu, Xiwei Wu, and Qinxiang Cao. 2025. Encode the∀∃ Relational Hoare Logic into Standard Hoare Logic. arXiv:2504.17444 [cs.PL] https://arxiv.org/abs/2504.17444

    2025 arXiv

  50. [62]

    Linpeng Zhang, Noam Zilberstein, Benjamin Lucien Kaminski, and Alexandra Silva. 2024. Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers.Proc. ACM Program. Lang.8, OOPSLA2 (2024), 817–845. https://doi.org/10.1145/3689740

    2024 doi

  51. [63]

    Noam Zilberstein, Derek Dreyer, and Alexandra Silva. 2023. Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning.Proc. ACM Program. Lang.7, OOPSLA1 (2023). https://doi.org/10.1145/3586045

    2023 doi

  52. [64]

    Noam Zilberstein, Dexter Kozen, Alexandra Silva, and Joseph Tassarotti. 2025. A Demonic Outcome Logic for Randomized Nondeterminism.Proc. ACM Program. Lang.9, POPL (2025), 539–568. https://doi.org/10.1145/3704855

    2025 doi

  53. [2023]

    ACM Program

    An Algebra of Alignment for Relational Verification.Proc. ACM Program. Lang.7, POPL, Article 20 (2023), 30 pages. https://doi.org/10.1145/3571213 Full version at https://arxiv.org/abs/2202.04278

    2023 arXiv

Pith tools

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