Relational verification encompasses information flow security, regression verification, translation validation for compilers, and more. Effective alignment of the programs and computations to be related facilitates use of simpler relational invariants and relational procedure specs, which in turn enables automation and modular reasoning. Alignment has been explored in terms of trace pairs, deductive rules of relational Hoare logics (RHL), and several forms of product automata. This article shows how a simple extension of Kleene Algebra with Tests (KAT), called BiKAT, subsumes prior formulations, including alignment witnesses for forall-exists properties, which brings to light new RHL-style rules for such properties. Alignments can be discovered algorithmically or devised manually but, in either case, their adequacy with respect to the original programs must be proved; an explicit algebra enables constructive proof by equational reasoning. Furthermore our approach inherits algorithmic benefits from existing KAT-based techniques and tools, which are applicable to a range of semantic models.

翻译：关系验证涵盖信息流安全、回归验证、编译器翻译验证等多个领域。有效对齐待关联的程序与计算过程，有助于采用更简单的关系型不变量和关系型过程规约，进而实现自动化与模块化推理。此前，对齐方法已在迹对、关系霍尔逻辑（RHL）演绎规则及多种形式的乘积自动机中得到探索。本文表明，通过一种名为BiKAT的带测试的Kleene代数（KAT）的简单扩展，可涵盖先前的各种形式化方法（包括针对forall-exists属性的对齐证据），并为此类属性提出新的RHL风格规则。对齐既可算法化自动发现，也可手动设计，但无论采用何种方式，都必须证明其与原始程序之间的充分性；显式代数结构支持通过等式推理进行构造性证明。此外，我们的方法继承了现有基于KAT的技术与工具在算法层面的优势，这些方法适用于多种语义模型。