TY - GEN
T1 - Alignment Completeness for Relational Hoare Logics
AU - Nagasamudram, Ramana
AU - Naumann, David A.
N1 - Publisher Copyright: © 2021 IEEE.
PY - 2021/6/29
Y1 - 2021/6/29
N2 - Relational Hoare logics (RHL) provide rules for reasoning about relations between programs. Several RHLs include a rule we call sequential product that infers a relational correctness judgment from judgments of ordinary Hoare logic (HL). Other rules embody sensible patterns of reasoning and have been found useful in practice, but sequential product is relatively complete on its own (with HL). As a more satisfactory way to evaluate RHLs, a notion of alignment completeness is introduced, in terms of the inductive assertion method and product automata. Alignment completeness results are given to account for several different sets of rules. The notion may serve to guide the design of RHLs and relational verifiers for richer programming languages and alignment patterns.
AB - Relational Hoare logics (RHL) provide rules for reasoning about relations between programs. Several RHLs include a rule we call sequential product that infers a relational correctness judgment from judgments of ordinary Hoare logic (HL). Other rules embody sensible patterns of reasoning and have been found useful in practice, but sequential product is relatively complete on its own (with HL). As a more satisfactory way to evaluate RHLs, a notion of alignment completeness is introduced, in terms of the inductive assertion method and product automata. Alignment completeness results are given to account for several different sets of rules. The notion may serve to guide the design of RHLs and relational verifiers for richer programming languages and alignment patterns.
UR - https://www.scopus.com/pages/publications/85110491842
UR - https://www.scopus.com/pages/publications/85110491842#tab=citedBy
U2 - 10.1109/LICS52264.2021.9470690
DO - 10.1109/LICS52264.2021.9470690
M3 - Conference contribution
T3 - Proceedings - Symposium on Logic in Computer Science
BT - 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021
Y2 - 29 June 2021 through 2 July 2021
ER -