Many interesting program properties involve the
execution of multiple programs,
including observational equivalence,
noninterference, co-termination, monotonicity,
and idempotency. One popular approach to
reasoning about these sorts of relational
properties is to construct and verify a
product program: a program whose
correctness implies that the individual programs
exhibit the desired relational property. A key
challenge in product program construction 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 product program construction that
uses e-graphs, equality saturation, and
algebraic realignment rules to efficiently
represent and build verifiable product
programs. A key ingredient of our solution is a
novel data-driven extraction technique that uses
execution traces of product programs to identify
candidate 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.