KestRel: Relational Verification Using E-Graphs for Program Alignment

TL;DR

KestRel introduces a novel e-graph-based method for constructing intermediate programs that facilitate the automated verification of relational properties between multiple programs, leveraging execution traces for semantic alignment.

Contribution

The paper presents a new approach using e-graphs and execution trace analysis to automatically generate aligned intermediate programs for relational verification.

Findings

Effective in verifying various relational properties.

Improves alignment accuracy through data-driven techniques.

Demonstrates scalability on benchmark suite.

Abstract

Many interesting program properties involve the execution of multiple programs, including observational equivalence, noninterference, co-termination, monotonicity, and idempotency. One strategy for verifying such relational properties is to construct and reason about an intermediate program whose correctness implies that the individual programs exhibit those properties. A key challenge in building an intermediate program is finding a good alignment of the original programs. An alignment puts subparts of the original programs into correspondence so that their similarities can be exploited in order to simplify verification. We propose an approach to intermediate program construction that uses e-graphs, equality saturation, and algebraic realignment rules to efficiently represent and build programs amenable to automated verification. A key ingredient of our solution is a novel data-driven extraction technique that uses execution traces of candidate intermediate programs to identify solutions that are semantically well-aligned. We have implemented a relational verification engine based on our proposed approach, called KestRel, and use it to evaluate our approach over a suite of benchmarks taken from the relational verification literature.