An Algebra of Alignment for Relational Verification
An Algebra of Alignment for Relational Verification
复制标题
关系验证的对齐代数
DOI：
10.1145/3571213
复制
发表时间：
2023
影响因子：
--
通讯作者：
Ngo, Minh
中科院分区：
文献类型：
--
作者：
Antonopoulos, Timos;Koskinen, Eric;Le, Ton Chanh;Nagasamudram, Ramana;Naumann, David A.;Ngo, Minh
关系验证包括信息流安全性、回归验证、编译器的转换验证等。程序和计算的有效对齐有助于使用更简单的关系不变量和关系过程规范，这反过来又使自动化和模块化推理成为可能。对齐已被探索的痕迹对，演绎规则的关系霍尔逻辑（RHL），和几种形式的产品自动机。本文展示了一个简单的扩展Kleene代数与测试（KAT），称为BiKAT，包含先前的公式，包括对齐证人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.
登录
查看更多内容
关系霍尔逻辑三十七年：对其原理和历史的评论
DOI：
--
发表时间：
2020
期刊：
Verification and Validation
影响因子：
--
作者：
Naumann, David A
通讯作者：
Naumann, David A
分离与还原
DOI：
--
发表时间：
2000
期刊：
International Conference on Mathematics of Program Construction
影响因子：
--
作者：
Ernie Cohen
通讯作者：
Ernie Cohen
动力学模型理论的一些结果
影响因子：
1.3
作者：
D. Kozen
通讯作者：
D. Kozen
Kleene 代数与测试和程序的静态分析
DOI：
--
发表时间：
2003
期刊：
影响因子：
--
作者：
D. Kozen
通讯作者：
D. Kozen
计算机辅助设计的形式化方法 (FMCAD)，2012
DOI：
--
发表时间：
2012
期刊：
影响因子：
--
作者：
G. Cabodi;Satnam Singh
通讯作者：
Satnam Singh