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.