pith. sign in

arxiv: 1907.03997 · v1 · pith:OSCLH34Wnew · submitted 2019-07-09 · 💻 cs.PL · cs.LO

Relational Verification via Invariant-Guided Synchronization

Qi Zhou (Georgia Institute of Technology) , David Heath (Georgia Institute of Technology) , William Harris (Galois Inc.) This is my paper

Pith reviewed 2026-05-25 00:04 UTC · model grok-4.3

classification 💻 cs.PL cs.LO
keywords relational verificationinvariant synthesissynchronization pointsprogram equivalenceJVM bytecoderelational propertiesautomated verification
0
0 comments X

The pith

Searching for synchronization points and synthesizing relational invariants simultaneously verifies properties that defeat heuristic-based methods.

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

The paper proposes a method for verifying relational properties such as functional equivalence across multiple program executions. Instead of first picking synchronization points with syntax-based heuristics and then trying to find invariants, the method searches for the points and synthesizes the invariants at the same time, letting the growing invariants steer the choice of points toward ones that admit complete proofs. The approach is realized in the PEQUOD tool for JVM bytecode and is shown to succeed on verification tasks drawn from the literature and from student challenge problems where existing techniques fail.

Core claim

By synthesizing relational invariants simultaneously with the search for synchronization points and using the invariants to guide selection of those points, the method produces complete proofs of relational properties even when conventional syntax-based heuristic selection of synchronization points leads only to invariants that are too complicated or inexpressible in the target theory.

What carries the argument

Invariant-guided synchronization: the simultaneous synthesis of relational invariants to steer the discovery of synchronization points that permit complete proofs.

If this is right

  • Relational verification tasks previously unsolvable by heuristic synchronization become feasible.
  • Proofs can succeed with invariants that remain expressible in the target theory.
  • The method applies directly to JVM bytecode programs from research benchmarks and student submissions.
  • Verification of functional equivalence and similar relational properties improves in coverage.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The technique may generalize to languages other than JVM bytecode if the underlying invariant synthesizer is replaced.
  • Security properties such as non-interference could be targeted by encoding them as relational invariants.
  • Integration with existing static analyzers might allow the simultaneous search to scale to larger codebases.

Load-bearing premise

Synthesizing relational invariants at the same time as searching for synchronization points will locate points that yield complete proofs where purely heuristic selection fails.

What would settle it

A relational property known to hold for two JVM programs where PEQUOD reports no proof exists while a heuristic-first tool produces one, or a property where PEQUOD succeeds only because of the simultaneous synthesis.

Figures

Figures reproduced from arXiv: 1907.03997 by David Heath (Georgia Institute of Technology), Qi Zhou (Georgia Institute of Technology), William Harris (Galois Inc.).

Figure 1
Figure 1. Figure 1: tri0 and tri1: equivalent programs that, given integer n, compute the nth triangle number. 1 public static int tri0_0 (int n) { 2 if (n <= 0) return 0; 3 else return n + tri0_1(n - 1); } 4 public static int tri0_1 (int n) { 5 if (n <= 0) return 0; 6 else return n + tri0_2(n - 1); } 7 public static int tri0_2 (int n) { 8 if (n <= 0) return 0;} 1 public static int tri1_0(int n) { 2 return tri1Aux_0(n, 0); } … view at source ↗
Figure 2
Figure 2. Figure 2: tri00 and tri10 are under-approximations of the input programs. tri1 makes use of an auxilliary procedure, tri1Aux, which maintains an accumulator. Despite these differences, these two programs compute the same function. To verify this equivalence, we can construct a relational property that shows that given equal parame￾ters n, tri0 and tri1 compute the same output. This property can be represented as a H… view at source ↗
Figure 3
Figure 3. Figure 3: Intermediate products that appear when proving th [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Operational semantics of programs in Com. When PEQUOD cannot find a valid proof for the original programs, PEQUOD increases the bounding number and starts over. The algorithm that generalizes bounded proofs is described in §4.2.3. 3 Background In this section, we present the technical background for our approach. In §3.1, we formalize the im￾perative target language. In §3.2, we introduce Constrained Horn … view at source ↗
Figure 5
Figure 5. Figure 5: Proof judgments for determining the validity of inv [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: The results of our evaluation of PEQUOD. Each benchmark is labeled with its source, name, the class of relational property that PEQUOD attempted to verify, time spent by PEQUOD to synthe￾size a proof, the peak amount of memory that PEQUOD used, and whether automated induction [23] or VeriMapRel [12] verified the benchmark. A time of TO denotes that PEQUOD was unable to con￾verge within 300 seconds. The sup… view at source ↗
read the original abstract

Relational properties describe relationships that hold over multiple executions of one or more programs, such as functional equivalence. Conventional approaches for automatically verifying such properties typically rely on syntax-based, heuristic strategies for finding synchronization points among the input programs. These synchronization points are then annotated with appropriate relational invariants to complete the proof. However, when suboptimal synchronization points are chosen the required invariants can be complicated or even inexpressible in the target theory. In this work, we propose a novel approach to verifying relational properties. This approach searches for synchronization points and synthesizes relational invariants simultaneously. Specifically, the approach uses synthesized invariants as a guide for finding proper synchronization points that lead to a complete proof. We implemented our approach as a tool named PEQUOD, which targets Java Virtual Machine (JVM) bytecode. We evaluated PEQUOD by using it to solve verification challenges drawn from the from the research literature and by verifying properties of student-submitted solutions to online challenge problems. The results show that PEQUOD solve verification problems that cannot be addressed by current techniques.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper proposes PEQUOD, a tool for relational verification of JVM bytecode that simultaneously searches for synchronization points between programs and synthesizes relational invariants to guide the search, claiming this invariant-guided approach solves verification problems (such as functional equivalence) that cannot be addressed by current syntax-based heuristic techniques.

Significance. If the central empirical claim holds after strengthening the evaluation, the work would be significant for relational verification: it directly targets the known limitation that suboptimal synchronization points lead to inexpressible invariants, and the simultaneous synthesis strategy could enable proofs for instances intractable under prior methods.

major comments (2)
  1. [Abstract] Abstract (and evaluation): the claim that 'PEQUOD solve verification problems that cannot be addressed by current techniques' is load-bearing for the novelty result but is not secured, because the manuscript provides no evidence that baseline tools received exhaustive heuristic search, alternative synchronization strategies, or increased timeouts; without such controls the uniqueness of the solved instances cannot be established.
  2. [Abstract] The central algorithmic description (simultaneous invariant synthesis guiding synchronization search) is presented at a high level in the abstract with no details on the search procedure, invariant synthesis algorithm, or soundness argument, making it impossible to assess whether the approach supports the claim that it identifies synchronization points leading to complete proofs where heuristics fail.
minor comments (1)
  1. [Abstract] Abstract contains duplicated phrasing ('from the from the research literature') and a subject-verb agreement error ('PEQUOD solve' should be 'PEQUOD solves').

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback. We address the two major comments point by point below and indicate where revisions will be made to strengthen the manuscript.

read point-by-point responses

  1. Referee: [Abstract] Abstract (and evaluation): the claim that 'PEQUOD solve verification problems that cannot be addressed by current techniques' is load-bearing for the novelty result but is not secured, because the manuscript provides no evidence that baseline tools received exhaustive heuristic search, alternative synchronization strategies, or increased timeouts; without such controls the uniqueness of the solved instances cannot be established.

    Authors: We agree that the evaluation does not report exhaustive heuristic searches or extended timeouts on the baselines. To secure the claim, we will add a new subsection to the evaluation that applies more comprehensive synchronization heuristics and longer timeouts to the baseline tools on the same benchmark set, reporting any newly solved instances. This will directly address the concern about uniqueness. revision: yes

  2. Referee: [Abstract] The central algorithmic description (simultaneous invariant synthesis guiding synchronization search) is presented at a high level in the abstract with no details on the search procedure, invariant synthesis algorithm, or soundness argument, making it impossible to assess whether the approach supports the claim that it identifies synchronization points leading to complete proofs where heuristics fail.

    Authors: The abstract is intentionally high-level per standard conventions for the venue. The search procedure, invariant synthesis algorithm (including the use of synthesized invariants to guide synchronization), and soundness argument are detailed in Sections 3 and 4, with the key lemmas and theorems stated there. We will revise the abstract to include one additional sentence summarizing the simultaneous search strategy while remaining within length limits. revision: partial

Circularity Check

0 steps flagged

No circularity; approach and evaluation are self-contained

full rationale

The paper defines a search procedure that interleaves synchronization-point discovery with invariant synthesis and evaluates the resulting tool PEQUOD on external benchmarks drawn from the literature and student submissions. No equations, fitted parameters, or predictions appear in the provided text. The central claim (that the method succeeds on instances where prior techniques fail) is an empirical statement about tool performance rather than a derivation that reduces to its own inputs by construction. No self-citations are invoked as load-bearing uniqueness theorems, and the algorithm is presented as an independent heuristic rather than a renaming or re-derivation of prior results. This satisfies the default expectation of a non-circular systems paper.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

No free parameters or invented entities identified from the abstract. The approach rests on the domain assumption that invariant synthesis can effectively guide synchronization point discovery.

axioms (1)
  • domain assumption Synthesized relational invariants can guide discovery of synchronization points that enable complete proofs
    This is the core mechanism proposed to overcome limitations of heuristic synchronization selection.

pith-pipeline@v0.9.0 · 5717 in / 1008 out tokens · 23025 ms · 2026-05-25T00:04:22.151337+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages

  1. [1]

    In: ICFP, doi:10.1145/3110265

    Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deep ak Garg & Pierre-Yves Strub (2017): A Relational Logic for Higher-Order Programs. In: ICFP, doi:10.1145/3110265

    work page doi:10.1145/3110265 2017

  2. [2]

    McMillan (2013): Beautiful Interpolants

    A ws Albarghouthi & Kenneth L. McMillan (2013): Beautiful Interpolants . In: CA V, doi:10.1007/978-3-642-39799-8_22

    work page doi:10.1007/978-3-642-39799-8_22 2013

  3. [3]

    Naumann Anindya Banerjee & Mohammad Nikouei (20 16): Relational Logic with Framing and Hypotheses

    David A. Naumann Anindya Banerjee & Mohammad Nikouei (20 16): Relational Logic with Framing and Hypotheses. In: FSTTCS, doi:10.4230/LIPIcs.FSTTCS.2016.11

    work page doi:10.4230/lipics.fsttcs.2016.11 2016

  4. [4]

    Backes, Suzette Person, Neha Rungta & Oksana Tkac huk (2013): Regression V erification Using Impact Summaries

    John D. Backes, Suzette Person, Neha Rungta & Oksana Tkac huk (2013): Regression V erification Using Impact Summaries. In: SPIN, doi:10.1007/978-3-642-39176-7_7

    work page doi:10.1007/978-3-642-39176-7_7 2013

  5. [5]

    In: FM, doi:10.1007/978-3-642-21437-0_17

    Gilles Barthe, Juan Manuel Crespo & César Kunz (2011): Relational V erification Using Product Programs. In: FM, doi:10.1007/978-3-642-21437-0_17. 1https://www.dropbox.com/s/yks0eyic8dsf69e/pequod.zip?dl=0 Q. Zhou, D. Heath, & W. Harris 41

    work page doi:10.1007/978-3-642-21437-0_17 2011

  6. [6]

    In: LNCS, doi:10.1007/978-3-642-35722-0_3

    Gilles Barthe, Juan Manuel Crespo & César Kunz (2013): Beyond 2-Safety: Asymmetric Product Programs for Relational Program V erification. In: LNCS, doi:10.1007/978-3-642-35722-0_3

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

  7. [7]

    In: JLAMP, doi:10.1016/j.jlamp.2016.05.004

    Gilles Barthe, Juan Manuel Crespo & César Kunz (2016): Product Programs and Relational Program Logics. In: JLAMP, doi:10.1016/j.jlamp.2016.05.004

    work page doi:10.1016/j.jlamp.2016.05.004 2016

  8. [8]

    D’Argenio & Tamara Rezk (2004): Secure Information Flow by Self-Composition

    Gilles Barthe, Pedro R. D’Argenio & Tamara Rezk (2004): Secure Information Flow by Self-Composition . In: CSFW-17, doi:10.1017/S0960129511000193

    work page doi:10.1017/s0960129511000193 2004

  9. [9]

    In: ITP, doi:10.1007/978-3-642-22863-6_6

    Lennart Beringer (2011): Relational Decomposition. In: ITP, doi:10.1007/978-3-642-22863-6_6

    work page doi:10.1007/978-3-642-22863-6_6 2011

  10. [10]

    McMillan & Andrey Rybalche nko (2013): On Solving Universally Quantified Horn Clauses

    Nikolaj Bjørner, Kenneth L. McMillan & Andrey Rybalche nko (2013): On Solving Universally Quantified Horn Clauses. In: SAS, doi:10.1007/978-3-642-38856-9_8

    work page doi:10.1007/978-3-642-38856-9_8 2013

  11. [11]

    Marcel Böhme, Bruno C. d. S. Oliveira & Abhik Roychoudhu ry (2013): Partition-based regression verifica- tion. In: ICSE, doi:10.1109/ICSE.2013.6606576

    work page doi:10.1109/icse.2013.6606576 2013

  12. [12]

    In: CILC

    Alberto Pettorossi Emanuele De Angelis, Fabio Fiorava nti & Maurizio Proietti (2016): V erifying Relational Program Properties by Transforming Constrained Horn Claus es. In: CILC

    work page 2016

  13. [13]

    In: ASE, doi:10.1145/2642937.2642987

    Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Phi lipp Rümmer & Mattias Ulbrich (2014): Automating regression verification. In: ASE, doi:10.1145/2642937.2642987

    work page doi:10.1145/2642937.2642987 2014

  14. [14]

    In: DAC, doi:10.1145/1629911.1630034

    Benny Godlin & Ofer Strichman (2009): Regression verification. In: DAC, doi:10.1145/1629911.1630034

    work page doi:10.1145/1629911.1630034 2009

  15. [15]

    Lahiri & Henrique Rebêlo (2013): T o- wards Modularly Comparing Programs Using Automated Theore m Provers

    Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri & Henrique Rebêlo (2013): T o- wards Modularly Comparing Programs Using Automated Theore m Provers . In: CADE-24, doi:10.1007/978-3-642-38574-2_20

    work page doi:10.1007/978-3-642-38574-2_20 2013

  16. [16]

    https://leetcode.com/

    (2016): LeetCode Online Judge. https://leetcode.com/. Accessed: 2015 Nov 16

    work page 2016

  17. [17]

    Lopes & José Monteiro (2016): Automatic equivalence checking of programs with uninterpr eted functions and integer arithmetic

    Nuno P . Lopes & José Monteiro (2016): Automatic equivalence checking of programs with uninterpr eted functions and integer arithmetic . STTT 18(4), doi:10.1007/s10009-015-0366-1

    work page doi:10.1007/s10009-015-0366-1 2016

  18. [18]

    Journal of Automated Reasoning 60(3), doi:10.1007/s10817-017-9433-5

    Mattias Ulbrich Moritz Kiefer, Vladimir Klevanov (201 6): Relational Program Reasoning Using Compiler IR. In: VSTTE, doi:10.1007/s10817-017-9433-5

    work page doi:10.1007/s10817-017-9433-5

  19. [19]

    In: CA V, doi:10.1007/978-3-319-96145-3_9

    Lauren Pick, Grigory Fedyukovich & Aartic Gupta (2018) : Exploiting Synchrony and Symmetry in Relational V erification. In: CA V, doi:10.1007/978-3-319-96145-3_9

    work page doi:10.1007/978-3-319-96145-3_9 2018

  20. [20]

    Pierce, Arthur Azevedo de Amorim, Chris Cas inghino, Marco Gaboardi, Michael Greenberg, Cˇatˇalin Hri¸ tcu, Vilhelm Sjöberg & Brent Y orgey (2018):Logical F oundations

    Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Cas inghino, Marco Gaboardi, Michael Greenberg, Cˇatˇalin Hri¸ tcu, Vilhelm Sjöberg & Brent Y orgey (2018):Logical F oundations. Software Foundations series, volume 1, Electronic textbook. V ersion 5.5. http://www.cis.upenn.edu/~bcpierce/sf

    work page 2018

  21. [21]

    In: PLDI, doi:10.1145/2980983.2908092

    Marcelo Sousa & Isil Dillig (2016): Cartesian Hoare logic for verifying k-safety properties . In: PLDI, doi:10.1145/2980983.2908092

    work page doi:10.1145/2980983.2908092 2016

  22. [22]

    In: SAS, doi:10.1007/11547662_24

    Tachio Terauchi & Alexander Aiken (2005): Secure Information Flow as a Safety Problem . In: SAS, doi:10.1007/11547662_24

    work page doi:10.1007/11547662_24 2005

  23. [23]

    In: CA V, doi:10.1007/978-3-319-63390-9_30

    Hiroshi Unno & Sho Torii (2017): Automating Induction for Solving Horn Clauses . In: CA V, doi:10.1007/978-3-319-63390-9_30

    work page doi:10.1007/978-3-319-63390-9_30 2017

  24. [24]

    https://github.com/Z3Prover/z3

    (2017): Z3Prover/z3 - GitHub. https://github.com/Z3Prover/z3. Accessed: 2017 July 1

    work page 2017