TY - JOUR
T1 - An Algebra of Alignment for Relational Verification
AU - Antonopoulos, Timos
AU - Koskinen, Eric
AU - Le, Ton Chanh
AU - Nagasamudram, Ramana
AU - Naumann, David A.
AU - Ngo, Minh
N1 - Publisher Copyright:
© 2023 Owner/Author.
PY - 2023/1/9
Y1 - 2023/1/9
N2 - 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.
AB - 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.
KW - Kleene algebra with tests
KW - hyperproperties
KW - program algebra
KW - relational verification
UR - http://www.scopus.com/inward/record.url?scp=85146628676&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85146628676&partnerID=8YFLogxK
U2 - 10.1145/3571213
DO - 10.1145/3571213
M3 - Article
AN - SCOPUS:85146628676
VL - 7
SP - 573
EP - 603
JO - Proceedings of the ACM on Programming Languages
JF - Proceedings of the ACM on Programming Languages
ER -