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.

翻译：关联验证包括信息流安全性、回归验证、编译器翻译验证等等。程序和计算的有效对齐有助于使用更简单的关联不变量及程序规范，从而实现自动化和模块化推理。对齐已经从迹对、关联Hoare逻辑的演绎规则和几种形式的乘积自动机等方面进行了探索。本文展示了一种名为BiKAT的Kleene测试代数的简单扩展，它包括了之前的形式，包括全称存在性质的对齐证明，这揭示了这类性质的新的关联Hoare逻辑规则。对齐可以通过算法自动发现或手动设计，但无论哪种情况，都必须证明其相对于原始程序的充分性；这种明确的代数可以通过等式推导进行构造性的证明。此外，我们的方法从现有的基于Kleene测试代数的技术和工具中继承了算法优势，这些技术和工具适用于一系列语义模型。