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.

翻译：许多有趣的程序属性涉及多个程序的执行，包括观察等价性、非干扰性、共终止性、单调性和幂等性。推理这类关系属性的主流方法是构造并验证一个乘积程序：该程序的正确性意味着原始程序满足所需的关系属性。乘积程序构造的一个关键挑战在于找到原始程序的良好对齐方式。对齐将原始程序的子部分建立对应关系，以便利用它们的相似性来简化验证。本文提出一种基于E-Graph、等式饱和及代数重排规则的乘积程序构造方法，能够高效表示并构建可验证的乘积程序。我们方法的核心是一种新颖的数据驱动提取技术，该技术利用乘积程序的执行轨迹来识别语义对齐良好的候选解。基于所提方法，我们实现了一个名为KestRel的关系验证引擎，并使用关系验证文献中的基准测试套件对其进行了评估。