一句话：提出用E-Graph与等式饱和构造中间程序，并以执行轨迹驱动抽取实现程序对齐的关系验证。
许多程序性质涉及多个程序的执行，如观察等价、非干涉、共同终止、单调性和幂等性。关系验证的一种策略是构造一个中间程序，使其正确性蕴含原程序具有这些关系性质；关键挑战在于找到良好的程序对齐，将原程序子部分对应起来以简化验证。本文提出基于E-Graph、等式饱和和代数重对齐规则来构造中间程序，从而高效表示并生成适合自动验证的程序。其核心是一种新颖的数据驱动抽取技术，利用候选中间程序的执行轨迹识别语义上良好对齐的解。作者实现了关系验证引擎KestRel，并在关系验证文献中的基准集上评估该方法。
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.
@article{paperbot3205,
title = {KestRel: Relational Verification using E-Graphs for Program Alignment},
author = {Robert Dickerson and Prasita Mukherjee and Benjamin Delaware},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720474}
}