一句话：提出 BiKAT 代数统一关系验证中的对齐表示，支持等式推理并导出 forall-exists 性质的 RHL 规则。
关系验证涵盖信息流安全、回归验证、编译器翻译确认等。有效对齐待关联程序及其计算，可简化关系不变式与过程规约，从而支持自动化和模块化推理。已有工作从迹对、关系霍尔逻辑（RHL）演绎规则及多种乘积自动机角度研究对齐。本文提出 BiKAT——带测试的 Kleene 代数（KAT）的简单扩展——统一刻画既有对齐形式，包括 forall-exists 性质的对齐见证，并由此揭示新的 RHL 风格规则。对齐可由算法发现或手工设计，但都需证明其相对于原程序的充分性；显式代数使这一证明可通过等式推理构造性地完成。该方法还继承基于 KAT 的算法与工具，可应用于多种语义模型。
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.
@article{paperbot2094,
title = {An Algebra of Alignment for Relational Verification},
author = {Timos Antonopoulos and Eric Koskinen and Ton Chanh Le and Ramana Nagasamudram and David A. Naumann and Minh Ngo},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571213}
}