Completely Automated Equivalence Proofs

TL;DR

Pequod is an automated tool that verifies partial program equivalence by synthesizing relational proofs and invariants, significantly improving verification capabilities for dissimilar program pairs without manual input.

Contribution

This work introduces Pequod, a fully automated verifier for partial program equivalence that synthesizes relational proofs and invariants without requiring relational summaries or synchronization points.

Findings

Successfully verified hundreds of student solution pairs.

Outperformed existing techniques in verifying dissimilar program pairs.

Applied to Java bytecode, demonstrating practical utility.

Abstract

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.