{'fraction_non_alphanumeric': 0.03270528437472614, 'fraction_numerical': 0.01780737884497415, 'mean_word_length': 4.467228823303948, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Completely Automated Equivalence Proofs

Verifying partial (i.e., termination-insensitive) equivalence of programs has significant practical applications in software development and education. Conventional equivalence verifiers typically rely on a combination of given relational summaries and suggested synchronization points; such information can be extremely difficult for programmers without a background in formal methods to provide for pairs of programs with dissimilar logic. In this work, we propose a completely automated verifier for determining partial equivalence, named Pequod. Pequod automatically synthesizes expressive proofs of equivalence conventionally only achievable via careful, manual constructions of product programs To do so, Pequod syntheses relational proofs for selected pairs of program paths and combines the per-path relational proofs to synthesize relational program invariants. To evaluate Pequod, we implemented it as a tool that targets Java Virtual Machine bytecode and applied it to verify the equivalence of hundreds of pairs of solutions submitted by students for problems hosted on popular online coding platforms, most of which could not be verified by existing techniques.


INTRODUCTION
In many practical contexts, determining if two programs are functionally equivalent is a critical problem. Prominent instances of this problem include determining (1) if a given program written in a high-level source language is equivalent to a given (typically optimized) program that executes on a target machine architecture [28,37], (2) if consecutive versions of a program module preserve critical program behavior, (3) if one given program is an obfuscation of the other, or (4) if a program provided by a student or hiring candidate in response to a challenge problem is equivalent to a trusted reference solution. Checking student solutions, in particular, is perhaps more critical than ever before, given increasing enrollments in computer science courses and the rapid development of online programming courses [42].
While verifying even only termination-insensitive (i.e., partial) equivalence has been the subject of a significant body of work, many previous techniques are either intended to be applied to verify equivalence of programs generated from particular transformations [28,33,37], or can only be applied to programs that use restricted control structures (e.g., are loop-free [24]) or data operations (e.g., only linear arithmetic on scalar data, without operations on dynamically-allocated memory [34,47]). Other approaches only generate proofs for a bounded number of control paths [36,38] or inputs [42].
One strategy that can potentially be followed to prove the equivalence of many programs is to reduce the problem of verifying equivalence of programs P 0 and P 1 to synthesizing a product program that soundly models all steps of P 0 and P 1 , accompanied by inductive invariants of the product program that imply the equivalence of P 0 and P 1 . Unfortunately, current approaches that follow such a strategy either only attempt to synthesize product programs in a class that is too 2016 restricted to prove equivalence of many practical programs, such as the class of sequential compositions [9,15,45], or require additional information about a target product program to be provided manually [6,10,17,19,44].
In this paper, we present a novel verifier for partial equivalence, named PEQUOD, which is not subject to the limitations given above. I.e., PEQUOD can be applied to pairs of programs with arbitrary control structure and that use arbitrary data operations, and can potentially synthesize proofs ranging over a class of product programs that is much more expressive than those that have been synthesized by previous automatic verifiers.
The key challenge addressed by PEQUOD is, given programs P 0 and P 1 , to synthesize both a product program of P 0 and P 1 and suitable inductive invariants automatically. Previous approaches either require the structure of a product program to be provided manually, or that first attempt to guess the structure of a product program using heuristics, and then synthesize invariants for the product program by adapting techniques used by automatic verifiers of safety properties. Unfortunately, it is difficult to communicate the requirements of a product program to users without experience in program analysis (such as novice programmers). Proposed heuristics can only be applied in practice to programs have syntactic similarities that typically only hold for multiple versions of the same program. However, it is difficult to develop heuristics that can be applied to programs that have been developed by independent developers, such as a solutions submitted by independent groups of students.
PEQUOD addresses this key challenge by synthesizing both the product program and its inductive invariants simultaneously. In particular, PEQUOD selectively enumerates control paths of P 0 paired with those of P 1 . For each enumerated pair of control paths p 0 and p 1 , PEQUOD first determines if some runs of the paths from equivalent inputs result in non-equivalent outputs, in which case it determines that P 0 and P 1 are not equivalent. Otherwise, PEQUOD efficiently synthesizes a proof that each run of p 0 and each run of p 1 from equivalent inputs result in equivalent outputs. PEQUOD combines proofs synthesized for multiple pairs of paths, and then attempts to extract from them a product program and its inductive invariants using a novel symbolic search algorithm. An extensive body of previous work has developed automatic verifiers that synthesize inductive invariants of a single program from invariants of program paths in order to prove that a program satisfies a given safety property [5,21,22,32]. The contribution of the proposed work is to adapt such a strategy to simultaneously synthesize a product program and its invariants in order to prove that given programs are equivalent.
We have implemented a prototype of PEQUOD that verifies the partial equivalence of programs given in Java Virtual Machine (JVM) bytecode and have applied PEQUOD to verify the partial equivalence of 369 pairs of solutions to challenge problems hosted on online coding platforms [13,27]. Implementations of previous automated equivalence verifiers could verify only one of pairs of programs that we found.
The rest of this paper is organized as follows. §2 provides an informal overview of our approach, PEQUOD, by example. §3 reviews the technical foundations for our work, and §4 presents PEQUOD in detail. §5 presents an empirical evaluation of PEQUOD. §6 compares PEQUOD to related work on equivalence verification, and §7 concludes.

OVERVIEW
In this section, we illustrate PEQUOD by example. In §2.1, we present as a running example a pair of programs that were submitted independently as solutions to an online coding problem. In §2.2, we give a proof that the two solutions are partially equivalent, expressed as relational invariants over pairs of control locations. In §2.3, we illustrate how PEQUOD synthesizes the proof automatically.  LeetCode [27]. The Climbing Stairs Problem is to take an integer n and return the number of distinct ways to climb n steps, where steps can be climbed one or two at a time. If n ≤ 1, then the solution is one.

Climbing Stairs: a coding challenge problem
climbStairs0 and climbStairs1 are two correct solutions to the problem, submitted by independent programmers. climbStairs0 first checks if its argument n is less than or equal to 1, and if so, immediately returns 1 (line 5). Otherwise, climbStairs0 executes a loop with counter i incremented from 2 to n (lines [9][10][11][12][13][14]. The loop maintains the invariant that at each step, sum stores the number of sequences in which to climb i stairs, cur stores the number of sequences in which to climb i − 1 stairs, and prev stores the number of sequences in which to climb i − 2 stairs. In each step through the loop, climbStairs0 copies the value in sum to cur (line 11), increments the value in sum by prev (line 12), and copies the value in cur to prev (line 13). climbStairs0 iterates until i ≥ n and then returns the value stored in cur (lines 15).
climbStairs1 is similar to climbStairs0, but maintains the invariant that the variable count2 stores the number of sequences in which to climb i − 1 stairs and count1 stores the number of sequences in which to climb i − 2 stairs. While count1 and count2 are used in climbStairs1 similarly to how cur and sum are used in climbStairs0, they are initialized to distinct values to establish ClimbStair1's loop invariant (lines 7-8). Given the same input, climbStairs1 performs one more iteration of its loop than climbStairs0.

Equivalence of climbStairs0 and climbStairs1
climbStairs0 and climbStairs1, when given equal inputs on which they terminate, exit in states with return equal values; i.e., the programs are partially equivalent.
PEQUOD, given programs P 0 and P 1 attempts to determine if they are partially equivalent by synthesizing a product program of P 0 and P 1 , denoted P ′ , accompanied by suitable inductive invariants [6][7][8]. A product program of P 0 and P 1 is a program in which each location is a pair of a location of P 0 and a location of P 1 and each state is a pair of a state of P 0 and a state of P 1 . In each step of execution, the product program chooses a stepping component program-either P 0 or P 1 -based on its state, and then non-deterministically chooses an instruction of the chosen component program on which to step. Thus, there are potentially infinitely many product programs of fixed programs P 0 and P 1 . Each product program has the same state space, but in each step, chooses the stepping program based on a different predicate on its current state.
The equivalence of P 0 and P 1 is certified by inductive invariants of P ′ (1) the invariant at the pair of initial locations of P 0 and P 1 is supported by the assumption that the components of state corresponding to P 0 and P 1 have equivalent 3 arguments; (2) the invariant at the pair of final locations of P 0 and P 1 supports the conclusion that the components of state corresponding to P 0 and P 1 have equivalent return values. Such invariants are represented as a map from each pair of locations to a formula over a vocabulary consisting of the variables of the two programs.
The programs climbStairs0 and climbStairs1 have proofs of equivalence, each structured as a product program accompanied by such inductive invariants. For one such proof, the product program climbStairs ′ , at each pair of identical line numbers, chooses to step on climbStairs0, and at all other pairs of locations, chooses to step on climbStairs1. We will now describe a proof of equivalence of climbStairs0 and climbStairs1 as inductive invariants of the fixed product program climbStairs ′ . However, a key feature of PEQUOD is that it does not require a fixed product program to be given manually or as the result of heuristics. Instead, PEQUOD synthesizes both a product program and its invariants simultaneously. Such a technique is essential for automatically verifying the equivalence of programs that, unlike the relatively simple examples of climbStairs0 and climbStairs1, have dissimilar control structure or data variables.
Inductive invariants of climbStairs ′ can be represented as a map from pairs of control locations to symbolic relations.
We give symbolic relations over key pairs of locations as formulas over a logical vocabulary consisting of variables that occur in climbStairs0 and climbStairs1, denoted with subscripts 0 and 1. In this paper, we only consider symbolic relations defined over constraints in linear arithmetic, because this is sufficient to axiomatize the semantics of the simple programs that we describe. Our implementation of PEQUOD for JVM bytecode synthesizes invariants in a more expressive logic that can describe states with dynamically-allocated objects and arrays, namely the combination of the theories of linear arithmetic and arrays.
The relational invariant over lines 2 and 2, denoted I (2, 2), establishes that the components of the state of climbStairs ′ for climbStairs0 and climbStairs1 have equal arguments. I.e., I (2, 2) is The relational invariant for line 5 in climbStairs0 and 5 in climbStairs1, denoted I (5, 5), establishes that any pair of states in climbStairs0 and climbStairs1 at such locations will result in states with equivalent return values. I.e., I (5, 5) The relational invariant for line 9 of climbStairs0 and line 9 of climbStairs1, denoted I (9, 9), establishes that for each run of climbStairs ′ , (1) the value of i in climbStairs0 is one greater than the value of i in climbStairs1, (2) the value of sum in climbStairs0 is equal to the value of count2 in climbStairs1, and (3) the values of n in climbStairs0 and climbStairs1 are equal. I.e., I (9, 9) is The relational invariant for line 15 of climbStairs0 and line 15 of climbStairs, denoted I (15, 15), establishes that the components of the state of climbStairs ′ for climbStairs0 and climbStairs1 have equal values in their return variables.
I.e., I (15,15) is The symbolic relations for the pairs of locations given above define inductive invariants for climbStairs ′ that are supported by the assumption that climbStairs0 and climbStairs1 execute from states with equal arguments, and that support the assertion that if climbStairs0 and climbStairs1 terminate, they have equal return values. Thus, the invariants are proof that climbStairs0 and climbStairs1 are partially equivalent.

Synthesizing a product program and its invariants
PEQUOD, given programs P 0 and P 1 , attempts to synthesize a product program of P 0 and P 1 accompanied by inductive invariants by iteratively maintaining invariants of sets of pairs of P 0 and P 1 's paths. If the invariants I are defined for a path p 0 of P 0 and path p 1 of P 1 , then I maps p 0 and p 1 to a symbolic relation between all pairs of states reached after P 0 executes p 0 and P 1 executes p 1 from states with equal arguments.
In each of PEQUOD's iterations, it determines if the maintained path-pair invariants I M define inductive invariants of some product program of P 0 and P 1 . In particular, for path-pair invariants I p , if the map LocRels[I p ] from each pair of locations L 0 and L 1 to the disjunction of invariants in I p for all pairs of paths ending with L 0 and L 1 are inductive invariants of some product program of P 0 and P 1 , then I p are inductive path-pair invariants. If PEQUOD finds a subset of bindings of I M (i.e., some restriction of I M ) that is inductive, then PEQUOD determines that P 0 and P 1 are equivalent. If not, PEQUOD selects a path p 0 of P 0 and p 1 of P 1 on which its maintained path-pair invariants are undefined, attempts to synthesize invariants for p 0 and p 1 , and if it finds such invariants, merges them with the maintained set of path-pair invariants to complete its current iteration. PEQUOD's algorithm is described in detail in §4.2.
E.g., PEQUOD, given climbStairs0 and climbStairs1, synthesizes inductive path-pair invariants for the programs over the following steps. PEQUOD chooses as initial path-pair invariants the empty map. PEQUOD then determines that ∅ does not define inductive path-pair invariants, using a procedure discussed informally below and given in detail in §4.2.2.
As a result, PEQUOD chooses p 0 as a path of climbStairs0 and p 1 as a path of climbStairs1 that have no path-pair invariant in ∅. PEQUOD then attempts to synthesize path-pair invariants for p 0 and p 1 .
PEQUOD could be adapted to use different path-selection algorithms, causing it to choose different pairs of complete paths. We will consider a scenario in which PEQUOD chooses p 0 and p 1 in particular, because those paths most clearly illustrate the operation of PEQUOD.
Proving equivalence of pairs of paths. After PEQUOD selects a pair of paths p 0 and p 1 that are undefined in its maintained set of path-pair invariants, PEQUOD determines if p 0 and p 1 are equivalent, and synthesizes path-pair invariants for p 0 and p 1 by issuing repeated queries to an interpolating theorem prover. PEQUOD synthesizes path-pair invariants for p 0 and p 1 that contain path-pair invariants for each prefix of p 0 paired with each prefix of p 1 . Each path-pair invariant for a pair of path prefixes is synthesized from a logical interpolant, generated by a query to an interpolating theorem prover. The definition of interpolants is reviewed in §3.2, Defn. 4; the reduction from synthesizing path-pair invariants to finding interpolants is given in §4.2.1.
E.g., to verify that path p 0 of climbStairs0 and path p 1 climbStairs1 are equivalent, PEQUOD synthesizes invariants for each pair of a prefix of p 0 with a prefix of p 1 . One such collection of invariants over pairs of prefixes is depicted in Figure 2.
From path-pair invariants to a product program and its invariants. After PEQUOD extends its maintained path-pair invariants to include path-pair invariants for chosen paths p 0 and p 1 , it inspects the extended path-pair invariants to determine if some restriction are inductive, using a novel algorithm described in §4.2.2.
However, I else are not inductive invariants for product program climbStairs ′ , because they map the pair of paths ( [2], [2]) to n 0 = n 0 , and are not defined for any pair of paths that contain line 5 in climbStairs0 and line 5 in climbStairs1. PEQUOD, given climbStairs0 and climbStairs1, determines that in fact no restriction of I p are inductive path-pair invariants. PEQUOD continues to determine the equivalence of climbStairs0 and climbStairs1 by choosing a pair of paths p ′ 0 of climbStairs0 and p ′ 1 climbStairs1 that each reach line 5. PEQUOD then synthesizes path-pair invariants I ′ p for p ′ 0 and p ′ 1 . PEQUOD then uses I p and I ′ p to synthesize path-pair invariants I ′′ p for both (p 0 , p 1 ) and (p ′ 0 , p ′ 1 ), determines that some restriction of I ′′ p are inductive invariants for the product program climbStairs ′ , and thus determines that climbStairs0 is equivalent to climbStairs1.

BACKGROUND
In this section, we review technical concepts on which our approach is based. In §3.1, we define a target language of imperative programs. In §3.2, we review concepts from formal logic.

Target language
In this section, we define the structure ( §3.1.1) and semantics ( §3.1.2) of a language of imperative programs.

Program structure. A program is a set of instructions that bind the results of computations to variables. Let
Locs be a space of control locations that contain a distinguished initial location INIT and final location FINAL. Let Vars be a space of program variables, which contains parameter variables Params and a return variable ret. Let Instrs be a space of program instructions.
There is no labeled instruction i ∈ P for which Pre[i] = FINAL. The space of programs is denoted Lang. For the remainder of this section, let P ∈ Lang denote a fixed, arbitrary program.

Program semantics.
A run of P is a sequence of states generated by a sequence of labeled instructions in which adjacent instructions have matching target and pre locations. Let the space of program values be the space of integers; i.e., the space of values is Vals = Z. An evaluation of all variables in Vars is a store; i.e., the space of stores is Stores = Vars → Vals. The practical implementation of PEQUOD verifies partial equivalence of programs that operate on objects and arrays combined with integers. In this paper, we primarily consider programs that operate over only integers, and describe how our implementation handles practical language features in §4.3.3.
The transition relation of an instruction need not be total: thus, labeled instructions can implement control branches using instructions that act as assume instructions.
A path of P is a sequence of control locations that are in adjacent labeled instructions of P.
The space of paths of P is denoted A run of a program P is a path and a sequence of stores Σ of equal length, such that adjacent stores in Σ satisfy transition relations of instructions at their corresponding locations in p.
Definition 2. Let Σ = σ 0 , . . . , σ n−1 ∈ Stores and L 0 , . . . , L n−1 ∈ Paths[P] be such that for each 0 ≤ i < n − 1, The space of runs of P is denoted Runs[P]. For each path p ∈ Paths[P], the runs r ∈ Runs[P] such that p is the path of r are the runs of p.
P 0 , P 1 ∈ Lang are partially equivalent if all complete runs of P 0 and P 1 that begin from stores in which parameters have equal values end in stores in which the return variables store equal values.
In order to simplify the presentation of our approach, we have given a definition of equivalence in terms of equality over identical parameter and return variables. However, our approach can be immediately generalized to take as a specification of equivalence any equivalence relation over input and final states of two programs. Because Defn. 3 defines equivalence in terms of equal input states and equal resulting output states, it can describe pairs of programs with different control structures and variables used for internal computation, such as climbStairs0 and climbStairs1 (introduced in §2.1).

Formal logic
PEQUOD uses formal logic to model the semantics of programs and represent invariants that relate their states. The quantifier-free fragment of the theory of linear arithmetic is denoted LIA. For each space of logical variables X , the space of LIA formulas over X is denoted Forms[X ]. For each formula φ ∈ Forms[X ], the set of variables that occur in φ (i.e., the vocabulary of φ) is denoted V(φ). A LIA model m over X is an assignment from each variable in X to an integer. The For all vectors of variables X = [x 0 , . . . , x n ] and Y = [y 0 , . . . , y n ], the LIA formula constraining the equality of each element in X with its corresponding element in Y , i.e., the formula 0≤i ≤n Although determining the satisfiability of a LIA formula is NP-complete in general, decision procedures for LIA have been proposed that often determine the satisfiability of formulas that arise from practical verification problems efficiently [14]. PEQUOD assumes access to a decision procedure for LIA, denoted ISSAT.
An interpolant of mutually inconsistent formulas φ 0 and φ 1 is a LIA formula that explains their inconsistency using their common vocabulary.

Definition 4. For spaces of logical variables
Previous work has introduced interpolating theorem provers that synthesize interpolants of pairs of mutuallyunsatisfiable formulas in extensions theories used to model program semantics and specifications [31]. To present PEQUOD, we assume access to a procedure ITP that, given mutually unsatisfiable LIA formulas φ 0 , φ 1 , returns an interpolant of φ 0 and φ 1 .
3.2.1 Symbolic representation of program semantics. The semantics of Lang can be represented symbolically using LIA formulas. In particular, each program store σ ∈ Stores corresponds to a LIA model over the vocabulary Vars, denoted m σ . For each space of variables X , space of indices I and index i ∈ I , the space of variables X i denotes a distinct copy of the variables in X . X ′ denotes primed copies of X , which will typically be used to model the post-state resulting from an instruction.
A symbolic relation is a formula whose models define pairs of states from distinct programs. The space of symbolic relations is denoted SymRels = Forms[Vars 0 , Vars 1 ].

TECHNICAL APPROACH
In this section, we describe our approach in technical detail. In §4.1, we define a class of proof structures that each represent a product program paired with its inductive invariants. In §4.2, we describe PEQUOD, which given two programs, attempts to prove or falsify their equivalence by synthesizing such a proof structure. In §4.3, we state and prove the correctness of PEQUOD, and compare it to related approaches for proving program equivalence. Proofs for each lemma and theorem stated in this section are given in Appendix A.

Proof structures
For fixed P 0 , P 1 ∈ Lang, location-pair invariants of P 0 and P 1 describe each pair of runs of P 0 and P 1 . Locationpair invariants are represented as a map from each pair of control locations to a symbolic relation that describes pairs of states of P 0 and P 1 at the mapped pair of locations. Let the space of location-pair relations be denoted LocRels = Locs × Locs → SymRels.
(3) for each L ∈ Locs and i ∈ P 1 , Then (I 0 , I 1 ) are location-pair invariants of P 0 and P 1 .
The space of location-pair invariants for P 0 and P 1 is denoted LocInvs[P 0 , P 1 ].
Location-pair invariants for P 0 and P 1 define both a product program P ′ for P 0 and P 1 , along with inductive invariants of P ′ that imply that P 0 ≡ P 1 , as described in §2.2. Let (I 0 , I 1 ) be location-pair invariants for P 0 and P 1 ; the product program P ′ defined by (I 0 , I 1 ) is as follows. For all L 0 , L 1 ∈ Locs, if P ′ is in a state that satisfies I 0 (L 0 , L 1 ), then P ′ may choose P 0 as 9 its stepping program; if P ′ is in a state that satisfies I 1 (L 0 , L 1 ), then P ′ may choose P 1 as its stepping program. Otherwise, the next step P ′ is undefined in its current state.
Example 1. climbStairs0 and climbStairs1 have location-pair invariants I 0 , I 1 ∈ LocRels that correspond to the product program climbStairs ′ and its inductive invariants given in §2.2. Key entries in I 0 include I 1 at each of the location pairs given above is False. At pairs of locations that are not the same line numbers in climbStairs0 and climbStairs1, I 0 is False and I 1 is a suitable symbolic relation.
Location-pair invariants for P 0 and P 1 are evidence of the partial equivalence of P 0 and P 1 .
PEQUOD attempts to synthesize location-pair invariants from maps from pairs of paths to symbolic relations. Let a path-pair relation be a partial map from pairs of paths to symbolic relations; i.e., the space of path-pair relations is Path-pair relations that (1) are supported by the assumption that runs of P 0 and P 1 begin with equal arguments, (2) soundly model steps of execution of P 0 , (3) soundly model steps of execution of P 1 , and (4) support the conclusion that all modeled pairs of complete paths end in states with equal return values are path-pair invariants.
Then I are path-pair invariants of P 0 and P 1 .
The space of path-pair invariants for P 0 and P 1 is denoted PathInvs If path-pair invariants I define a product program and inductive invariants that prove P 0 ≡ P 1 , then I are inductive for ∈ LocRels be such that for all L 0 , L 1 ∈ Locs, are location-pair invariants of P 0 and P 1 (Defn. 5), then I are inductive path-pair invariants for P 0 and P 1 .
Inductive path-pair invariants for P 0 and P 1 are evidence of partial equivalence, by Lemma 1. PEQUOD, given P 0 and P 1 , attempts to prove P 0 ≡ P 1 by synthesizing inductive path-pair invariants of P 0 and P 1 .
Input :P 0 , P 1 and I ∈ PathInvs[P 0 , P 1 ]. Output :HasInd to denote that some restriction of I are inductive path-pair invariants or a pair of paths not defined in I . 1 Procedure ChkInd(P 0 , P 1 , I )

Verification algorithm
Pseudocode for the core algorithm implemented by PEQUOD is given in Alg. 1. The core algorithm is structured as a counterexample-guided refinement loop analogous to conventional automatic verifiers of safety properties [11,32]. PEQUOD takes P 0 , P 1 ∈ Lang as input (line 1). PEQUOD defines a procedure PEQ' that, given I ∈ PathInvs[P 0 , P 1 ], attempts to determine if P 0 ≡ P 1 by constructing inductive path-pair invariants from I (line 2-line 13). PEQUOD runs PEQ' on the empty path-pair relation and returns the result (line 14).
PEQ', given path-pair invariants I (line 2), first runs a procedure CHKIND on P 0 , P 1 , and I (line 3). If CHKIND returns value HasInd to denote that some restriction of I are inductive path-pair invariants of P 0 and P 1 , then PEQ' returns True, to denote P 0 ≡ P 1 (line 4). Otherwise, if CHKIND returns a pair of paths p 0 and p 1 that are not defined in I (line 5), then PEQ' runs a procedure PATHINVS on P 0 , P 1 , p 0 and p 1 (line 6). If PATHINVS returns that p 0 p 1 , then PEQ' returns False, to denote P 0 P 1 (line 7).
Otherwise, if PATHINVS returns I ′ ∈ PathInvs[p 0 , p 1 ], then PEQ' runs MRG on I and I ′ to obtain path-pair invariants defined over all pairs of paths defined in I or I ′ , recurses on the result, and returns the result of the recursion (line 9).

4.2.1
Finding path-pair invariants using PathInvs. PATHINVS, given P 0 , P 1 ∈ Lang, p 0 ∈ Paths[P 0 ], and p 1 ∈ Paths[P 1 ], either returns path-pair invariants of p 0 and p 1 or determines that p 0 p 1 . PATHINVS attempts to find invariants of each p ′ 0 ∈ Prefixes[p 0 ] paired with each p ′ 1 ∈ Prefixes[p 1 ] as the interpolant of (1) the disjunction of path-pair invariants describing all pairs of states immediately before P 0 and P 1 take a final step to complete p ′ 0 and p ′ 1 and (2) a formula describing all pairs of states at p ′ 0 and p ′ 1 from which the remainder of p 0 and p 1 result in states with non-equal return values.
PATHINVS performs the following procedure. For each p ′ 0 ∈ Prefixes[p 0 ], let there be a distinct copy of Vars denoted ] be the conjunction of semantic constraints from all steps following in p 0 following p ′ 0 :  Pequod uses IsSat to determine that the above formula is unsatisfiable, and thus that the p 0 ≡ p 1 .
The second formula, referred to as the post-constraint Example 4. Pequod, given path p 0 of climbStairs0 and path p 1 of climbStairs (see §2.3), synthesizes the path-pair invariants of each prefix of p 0 paired with each prefix of p 1 using a series of queries to an interpolating theorem prover.
E.g., in order to synthesize the pair-pair invariant that relates prefix [2,9] of p 0 to prefix [2,9,9] of p 1 , Pequod synthesizes a pre-constraint consisting of the disjunction of (1) the path-pair invariant for ( [2], [2,9]) combined with the semantics of climbStairs0 stepping from 2 to 9 and (2) the path-pair invariant for ( [2,9], [2,9]) combined with the semantics of climbStairs1 taking a step from 9 to 9. Pequod computes the invariants for both of the pairs of paths given above from previous interpolation queries.
One interpolant of the pre-constraint and post-constraint given above is I (9, 9), the invariant for location 9 in climbStairs0 and 9 in climbStairs1 that is also a path-pair invariant for paths [2,9] and [2, 9,9], as depicted in Figure 2.

Finding inductive path-pair invariants using
ChkInd. Alg. 2 contains pseudocode for CHKIND. CHKIND, given P 0 , P 1 ∈ Lang and path-pair invariants I ∈ PathRels[P 0 , P 1 ] (line 1), returns either (1) the value HasInd to denote that some restriction of I is inductive path-pair invariants of P 0 and P 1 , or (2) a pair of paths of P 0 and P 1 that have no Otherwise, C' extends dis to contain (p 0 , p 1 ) to form dis ′ (line 8), and computes the result of recursing on dis ′ on three distinct sets of obligations: (1) obs ′ , the result of which is stored in r (line 9); (2) obs ′ extended with all control successors in P 0 of (p 0 , p 1 ) (denoted Ext(P 0 , p 0 )), the result of which is stored in r 0 (line 10); (3) obs ′ extended with all control successors in P 1 of (p 0 , p 1 ) (denoted Ext(P 1 , p 1 )), the result of which is stored in r 1 (line 11).
C' tests if I (p 0 , p 1 ) entails the invariant in I for some discharged pair of paths with the same final locations by computing: Pequod therefore returns a pair of complete paths p 0 and p 1 that includes 5 in climbStairs0 or line 5 in climbStairs1.
The correctness of PEQUOD is partially established partially by the fact that CHKIND returns HasInd only when given path-pair invariants that for which some restriction is inductive.

Discussion
In this section, we discuss several key properties of PEQUOD. In §4.3.1, we establish PEQUOD's correctness. In §4.3.2, we compare to PEQUOD a technique for proving partial equivalence given in previous work, self-composition. In §4.3.3, we describe challenges to designing a practical implementation of PEQUOD.

Correctness. Whenever PEQUOD returns a definite result, the result is correct.
Theorem 1. For all P 0 , P 1 ∈ Lang, if Pequod(P 0 , P 1 ) is defined, then P 0 ≡ P 1 if and only if Pequod(P 0 , P 1 ) = True.
Because determining partial program equivalence is, in general, undecidable, PEQUOD is not total: i.e., there are pairs of programs on which PEQUOD will not terminate. 14 PEQUOD as presented in Alg. 1, given P 0 , P 1 ∈ Lang, returns a Boolean decision as to whether P 0 ≡ P 1 . PEQUOD can be directly extended so that if it determines that P 0 ≡ P 1 , then it returns inductive path-pair invariants of P 0 and P 1 . In particular, CHKIND (Alg. 2) is extended so that given path-pair invariants I , if it determines that some restriction of I are inductive path-pair invariants of P 0 and P 1 , then it returns the restrictions of I that define location-pair invariants of P 0 and P 1 . In such a case, PEQUOD directly returns restrictions obtained from CHKIND. In order to return such restrictions of I , CHKIND maintains, in addition to the set of obligation path-pair obs, two sets of discharged pairs of paths, denoted dis 0 and dis 0 . When CHKIND calls itself on pairs of paths constructed from extensions of p 0 in P 0 (line 10), it extends dis 0 to contain (p 0 , p 1 ). When CHKIND calls itself on pairs of paths constructed from extensions of p 1 in P 1 (line 11), it extends dis 1 to contain (p 0 , p 1 ). When CHKIND determines if a given pair of paths (p 0 , p 1 ) has an invariant that is entailed by an invariant that has been previously discharged by computing the predicate IsDis, it enumerates over dis 0 ∪ dis 1 .
PEQUOD can also be directly extended so that if it determines that P 0 P 1 , then it returns a common input on which P 0 and P 1 generate different final values. To do so, PATHINVS is extended so that when it is given paths p 0 and p 1 such that NoEq[p 0 , p 1 ] ( §4.2.1) is satisfiable, PATHINVS returns one of its models, which is then returned directly by PEQUOD as a pair of runs from a common input that results in unequal return values.

Comparison to sequential composition. Previous work has proposed several approaches for automatically
determining the partial equivalence of programs. One approach that, given programs P 0 and P 1 , constructs the selfcomposition of P 0 and P 1 , which is a program that passes the same inputs to P 0 and P 1 , stores their results, and asserts that the results are equal [9,45]. Such an approach has potential applications for verifying that a program satisfies a desired information-flow property, can be formulated as proving that when a program is given two inputs with equivalent publicly-visible components, it generates outputs with equivalent publicy-visible components. However, such an approach typically cannot be applied to prove that two programs are partially equivalent, because it requires a safety prover to infer a summary for each of P and Q that precisely describes their functionality. Most model checkers use logics that are combinations of the quantifier-free fragments of linear arithmetic, uninterpreted functions, and arrays, which cannot express such summaries. In particular, neither climbStairs solutions given in §2, nor the solutions that we describe in §5 can be precisely summarized in such theories.

Practical design.
In §3.1.2, we defined the state space of a Langprogram to be a map from program variables to integer values. Our prototype implementation of PEQUOD can take as input programs represented in JVM bytecode, which use instructions that also dynamically allocate, load from, and store to dynamic memory and arrays. In order to support programs that execute such instructions, PEQUOD uses formulas that axiomatize the semantics of each instruction in the combination of the theory of linear arithmetic with the theory of arrays. Formulas in such theories can also be used to define equivalent initial or final states that contain linked data structures and arrays.
The key properties that must be satisfied by a theory T used by PEQUOD to axiomatize instructions are that (1) PEQUOD must have access to an interpolating theorem prover for T , which it uses to generate path-pair invariants ( §4.2.1); (2) PEQUOD must have access to an automatic decision procedure for T , used by PEQUOD to check entailments between pair-pair invariants of different path pairs in Alg. 2, line 12.
In §4.2, we described PEQUOD as using several procedures that were described only at the level of their interface, not their implementation. In particular, for fixed P ∈ Lang, the procedure CMPL, given p ∈ Paths[P], returns a complete extension of p. In general, a control path may have infinitely many complete extensions. Our prototype implementation of PEQUOD chooses a complete extension of minimum length, using breadth-first search.
The procedure CHOOSE, used in C' ( §4.2.2), given two results of recursive calls to C'-each of which may be either HasInd or a pair of control paths-returns a final result for the C'. Our prototype implementation of PEQUOD, given

EVALUATION
We performed an empirical evaluation of PEQUOD to answer the following questions: (1) Can PEQUOD verify the partial equivalence of programs written independently that implement distinct, subtle algorithms? (2) Can PEQUOD verify the partial equivalence of programs written by a wide set of independent programmers? (3) Can PEQUOD verify equivalence of programs more effectively than self-composition technical that using generic solver?
To answer the above experimental questions, we implemented PEQUOD as a partial-equivalence verifier for programs represented in JVM bytecode. While we presented PEQUOD in §4 as a verifier for programs whose instructions are defined in the theory of linear arithmetic, the actual implementation models core JVM language features, including arrays and objects, using the combined theory of linear arithmetic, arrays, and uninterpreted functions (AUFLIA). The only requirement imposed by PEQUOD on the logic for expressing program semantics is that the logic has (1) an effective decision procedure, which PEQUOD uses to check entailment over unknown predicates ( §4.2.2), and (2) an effective procedure that constructs interpolants, which PEQUOD uses to synthesize path-pair invariants ( §4.2.1). Both operations are supported by the Z3 interpolating theorem prover [48], which is used in our implementation. We applied PEQUOD to attempt to prove partial equivalence of 369 pairs of programs submitted by independent programmers as solutions to problems hosted on the online coding platforms Leetcode [27] and CodeChef [13].
In short, our experiments answer the above questions positively: PEQUOD was able to prove the partial equivalence of an overwhelming majority of pairs of programs to which it was applied. PEQUOD consistently proved the partial equivalence of programs more efficiently than self-composition technical that using generic solver. The results indicate that PEQUOD can synthesize proofs of partial equivalence effectively enough to be used as an educational aid, or as an underlying engine for other educational aids, such as autograders [42].

Experimental procedure
PEQUOD takes as input (1) two programs P 0 and P 1 , each represented as a JVM bytecode module. If PEQUOD determines P 0 ≡ P 1 , then it outputs the relational invariants of P 0 and P 1 as the proof. If PEQUOD determines that P 0 P 1 , it generates a pair of runs from P 0 and P 1 from a common input that result in outputs that are not equivalent. PEQUOD is implemented in 4, 932 lines of Java source code. PEQUOD uses the Soot analysis framework [43] to construct the control-flow graph of given programs, and uses the Z3 interpolating theorem prover [48] to synthesize path-pair invariants (see §4.2.1).
We collected as benchmarks programs submitted as solutions to problems posted on the coding platforms LeetCode The current version of PEQUOD cannot prove equivalence of the vast majority of solutions on such sites, as proofs of their equivalence require either quantified invariants over arrays or expressive heap invariants. While PEQUOD can model the semantics of such programs accurately, inferring sufficient invariants over data with such structure is itself an ongoing topic of research. We believe that combining PEQUOD with such approaches is an encouraging direction for future research.
In order to evaluate the ability of PEQUOD to prove equivalence compared to previous completely-automatic approaches, we implemented an equivalence verifier, named BASELINE, that uses self-composition (described in §4.3.2), to reduce equivalence verification to safety verification, and apply the best known techniques for safety verification. BASELINE, given programs P 0 and P 1 constructs systems of constrained Horn clauses [11] S 0 and S 1 that model all executions of P 0 and P 1 . BASELINE extends S 0 and S 1 to form a CHC system S ′ for which each solution corresponds to invariants of the self-composition of P 0 and P 1 that prove their equivalence. BASELINE then gives S ′ to DUALITY, a competitive CHC solver implemented within the z3 automated theorem prover.
Verifying equivalence of programs P 0 and P 1 can be reduced to verifying safety only if the P 0 and P 1 read input and write output to vectors of scalar data, not streams. As a result, we applied BASELINE to attempt to verify the equivalence of only programs that operate on scalar data. Such programs coincided exactly with the programs that we found on LeetCode.
Both PEQUOD and BASELINE were run on a machine with 16 1.4 GHz processors and 128 GB of RAM. The current implementation of PEQUOD uses a single thread. The implementation is publicly available [35]. All benchmarks are publicly available at references provided in this paper. All benchmarks were posted publicly by their programmers, and we have anonymized the sources of individual programs when referring to them in our results. We are working with the administrators of the coding platforms to potentially redistribute the collected solutions as a standard set of benchmarks for the verification community.

Equivalent solutions of challenge problems
In this section, we use example solutions from four challenge problems on LeetCode and CodeChef to illustrate PEQUOD's ability to synthesize proofs of equivalence of subtle implementations. In the relational invariants given for each pair of programs discussed, variables from the first programs (whose name ends with 0) are subscripted 0 and variables from the second program (whose name ends with 1) are subscripted 1. The Add Digits Problem [1] is to take a non-negative integer in variable num and return sum of all of the digits in num The Trailing Zeroes Problem [46] is, given a non-negative integer n, to to return the number of zero digits that occur before the least-significant non-zero digit in n!. PEQUOD proves that solutions TrailingZeroes0 ( Figure 5) and TrailingZeroes1 ( Figure 6) are equivalent by synthesizing the following relational invariant over their loop heads: The Reverse Integer Problem [39] is to take a non-negative integer n and return an integer that consists of the digits in n in reversed order. PEQUOD proves that solutions reverse0 (Figure 7) and reverse1 (Figure 8) are partially equivalent by synthesizing the following relational invariant over their loop heads: The Flow-001 Problem [16] is to read a non-negative integer T , then read T pairs of integers, printing the sum of each pair of integers. PEQUOD proves that two solutions given for the Flow-001 problem, FLOW001_0 ( Figure 9) and FLOW001_1 ( Figure 10

Results and conclusions
We ran PEQUOD to determine partial equivalence of the 369 program pairs collected. We also ran BASELINE to determine partial equivalence of the nine program pairs collected that did not operate on input and output streams. Because the rest of program pairs we collected has stream I/O that hard to express the assertion in self-composition technical.
The results are contained in Table 1. In Table 1, the first four problems are hosted on Leetcode [27] and the rest of the problems are hosted on CodeChef [13].
The only pair of programs that BASELINE can prove equivalent is the pair of solutions to the Add Digits problem. Both solutions to this problem have an input output relation that can be described precisely by a formula in linear arithmetic.
BASELINE is able to infer such a formula automatically. PEQUOD requires more time to infer such a solution for the solutions to Add Digits. However, the additional time required by PEQUOD to prove equivalence of a relatively simple pair of programs seems to be an acceptable cost to pay in many contexts in order to obtain the added power of PEQUOD for proving equivalence of more complex pairs of programs.
In summary, our results indicate that PEQUOD significantly improves the state of the art in verifying equivalence of concise, but subtle alternative implementations.

RELATED WORK
Verifying the equivalence of two programs can also be reduced to synthesizing and proving the correctness of a suitable product program [6,8]. Previous approaches construct the product program depending partly on matching control structures between the pairs of programs and establishing the logical equivalence of program conditions of matched structures. Previous work has also explored constructing asymmetric product programs [7] which can express proofs of equivalence between programs with loops. Such work does not address the problem of automatically inferring loop invariants of the synthesized product program, which may be viewed alternatively as relational invariants between loops of the original programs. This problem is directly addressed by PEQUOD.
For programs P 0 and P 1 , a special instance of the product programs of P 0 and P 1 is the sequential composition of P 0 and P 1 . Previous work has explored reducing verifying equivalence to constructing the self-composition of given programs and proving that it satisfies a suitable derived safety property [9,30,45] or synthesizing sequential summaries of the program by reduction to solving a system of constrained Horn clauses (CHCs) [15]. A key limitation of such approaches is that they can only infer proofs of correctness that can be expressed using summaries of each program's behavior in logic used by the verifier. Such logics typically are not sufficiently strong to express summaries required to prove the equivalence of non-trivial programs [6], including the solutions to programming problems that we encountered on online coding platforms [13,27]. PEQUOD attempts to synthesize relational invariants over internal control locations of two programs. Such a strategy enables PEQUOD to prove partial equivalence of a larger class of pairs of programs, both in principle (as discussed in §4.3.2) and in practice (as discussed in §5.3).
Previous work has proposed automatic verifiers of concurrent programs [18] that synthesize relational invariants by generating a CHC system that is discharged with a generic CHC solver [11,40]. PEQUOD is similar to such approaches in that it attempts to construct a proof of correctness from relational invariants over pairs of paths. PEQUOD is distinct from such approaches in that it uses a novel construction of relational invariants that can be used to prove partial equivalence of paths of independent programs (given in §4.2.1), and uses a novel algorithm that constructs pairs of relational invariants over locations based on relational invariants for pairs of paths (given in §4.2).
Several automatic equivalence checkers have been proposed for verifying the equivalence of affine [47] and numerical programs [34]. PEQUOD can be applied to programs that use any language features that can be axiomatized in a logical theory with interpolation, such as objects and arrays. PEQUOD does not require widening operations carefully tuned to particular numerical domains in order to converge.
Several proof systems have been proposed in both foundational [23] and modern work [19,44] for proving total program equivalence, simulation, and k-safety. For given programs P 0 and P 1 , such systems can express proofs of equivalence by establishing the validity of semantic summaries that relate the behavior of functions in P 0 and P 1 . Regression-verification techniques [17] match substructures of a pair of programs based on a traversal of the programs' syntactic structure and attempt to prove that matched substructures are equivalent, using provided candidate relational invariants. Regression verification can be optimized, using symbolic execution to only analyze slices of two given versions of a program that are changed [4]. Regression verification can also be applied to partitions of the given programs' input space, defined by path formulas of individual program paths, enabling programs to be proved equivalent gradually [12].
Recent work has provided logic systems for reasoning about relational properties of higher-order programs [2].
However, these systems have not yet been used to automatically synthesize proofs of program equivalence. PEQUOD can only infer proofs in a space of structures that is less expressive than the proof structures proposed in such work: in particular, the proofs inferred by PEQUOD are evidence of only partial equivalence. However, PEQUOD attempts to synthesize such proofs automatically.
Several approaches have been proposed that attempt to verify the equivalence of programs P 0 and P 1 by symbolically executing the paths of P 0 and P 1 . SYMDIFF verifies that given programs that are loop-free [24] or that are annotated with synchronization points [25] satisfy expected relational summaries. Unlike SYMDIFF, PEQUOD may not always terminate, but PEQUOD can be applied to potentially prove the partial equivalence of programs with loops. UCKLEE, similar to PEQUOD, symbolically executes both programs and inspects pairs of path formulas for control paths of P 0 and P 1 to determine if they are paths on which P 0 and P 1 are not equivalent [38]. However, PEQUOD can also potentially use the proofs of equivalence of a pair of paths to prove that given programs are equivalent.
A differential symbolic execution engine [36] symbolically executes given programs P 0 and P 1 , and can optionally construct a formula for each program that over-approximates the effect of each. The engine then compares the relational formulas for each program to determine if the programs may be equivalent. Such an engine is similar to PEQUOD, in that it uses symbolic reasoning to attempt to automatically synthesize a sound over-approximation of the effect of each program.
However, a key distinction between such an engine and PEQUOD is that PEQUOD infers relational invariants between programs by iteratively selecting and analyzing particular paths, rather than computing a fixed over-approximation of each program and then comparing the approximations.
Analyses for rootcausing failures of program equivalence [26] take a pair of control paths that prove the non-equivalence of two programs and generate a minimal-cost change to the programs that removes the feasibility of the counterexample.
Similarly to rootcausing analyses, PEQUOD applies a precise symbolic analysis to pairs of control paths from P 0 and P 1 .
Unlike rootcausing analyses, PEQUOD analyzes control paths either to determine that the paths are a true counterexample to equivalence or to synthesize path invariants that prove that the control paths are equivalent.
Several techniques have been proposed that improve the effectiveness of static program analyses by analyzing multiple versions of a program. The differential-assertion-checking problem [25] is to determine if one version of a given program analysis; these problems are distinct from the problem addressed by PEQUOD, which is to determine if two programs are partially equivalent. In particular, while PEQUOD also synthesizes an abstraction of given programs from interpolants, the interpolants are synthesized from proofs that pairs of paths from multiple programs are partially equivalent.
Some software model checkers select a program abstraction by constructing Craig interpolants [3,20,31,32,40] of sub-formulas of formulas that characterize runs of individual paths. However, unlike the above techniques PEQUOD uses interpolants to prove the equivalence of paths selected from distinct programs.
Previous work has identified equivalence verification as a problem with critical applications in programming education, and has proposed autograding techniques for automatically editing a student solution so that it is equivalent to a reference solution [42]. Existing work on autograding relies on a bounded model checker to determine if programs may be equivalent. An autograder that uses an improved equivalence verifier would enjoy a stronger soundness guarantee for determining when a student's solution is correct. An autograder designed to use not just counterexamples to equivalence but also relational invariants for equivalence could potentially suggest edits to student solutions that are functionally correct but could be simplified or optimized.

CONCLUSION
We have presented a novel algorithm that attempts to prove the partial equivalence of given programs. A key challenge in proving the partial equivalence of given programs P 0 and P 1 is to both synthesize a suitable product program P 1 of P 0 and P 1 , and to synthesize inductive invariants of P ′ that prove the equivalence of P 0 and P 1 . Previous approaches address this problem by first choosing a product program either by choosing one from a heavily restricted class of product programs, requiring a product program to be given manually, or choosing one based on fixed heuristics. After choosing a candidate product program, such approaches then attempt to synthesize its inductive invariants.
We have presented a novel equivalence verifier, named PEQUOD, that does not operate under any of the above limitations.
The key feature of PEQUOD is that it attempts to synthesize a product program and its invariants simultaneously. To do so, PEQUOD iteratively collects proofs of equivalence of pairs of paths of given programs, and attempts to extract a product program and its inductive invariants from the invariants defined per pair of paths. We have implemented a prototype version of PEQUOD that targets JVM bytecode, and used it to verify hundreds of alternate solutions submitted by students to online coding problems.
PROOF. There are two cases for this proof. The following is a proof of Lemma 3: PROOF. We construct this proof by induction on the evaluation of CHKIND run over obs and dis: The inductive claim is that if the path-pair invariants in obs are inductive, then there exists a restriction on I which is a set of inductive path-pair invariants that contains all elements of dis. For the inductive case, when obs is non-empty, a path-pair invariant I (p 0 , p 1 ) ∈ obs is inspected. obs ′ is constructed by removing I (p 0 , p 1 ) from obs, and dis ′ is constructed by adding I (p 0 , p 1 ) to dis. From here, there are two possibilities: If I (p 0 , p 1 ) is entailed by I (p ′ 0 , p ′ 1 ), p 0 and p ′ 0 end with the same control location, p 1 and p ′ 1 end with the same control location, and I (p ′ 0 , p ′ 1 ) ∈ dis then CHKIND calls itself recursively with obs ′ and dis ′ (Alg. 2, line 9). This step maintains the inductive claim. Location-pair invariants are constructed by taking the disjunction of all path-pair invariants that end with the same control location. This fact, the fact that p ′ 0 and p 1 end with the same control location as p 0 and p 1 , and the fact I (p ′ 0 , p ′ 1 ) entails I (p 0 , p 1 ) together indicate that I (p 0 , p 1 ) ∨ I (p ′ 0 , p ′ 1 ) still entails I (p 0 , p 1 ). Because I (p 0 , p 1 ) ∨ I (p ′ 0 , p ′ 1 ) hold for all clauses in the location-pair invariant system, the claim is established by definition of inductive path-pair invariants.
Otherwise, CHKIND calls itself recursively on obs ′ extended with the path-pair invariant from taking a step in the left program (Alg. 2, line 10) or in the right program (Alg. 2, line 11) together with dis ′ . In these cases, the claim is established by the definition of inductive invariants (Defn. 7) and the definition of location-pair invariants rules 2 and 3 respectively (Defn. 5).
When obs is empty, CHKIND returns HasInd, by Alg. 2. This fact, together with the inductive claim, implies that I is a set of inductive path-pair invariants for P 0 and P 1 . □ As stated by Thm. 1, whenever PEQUOD returns a definite result, the result is correct.