Alignment Completeness for Relational Hoare Logics

Ramana Nagasamudram; David A. Naumann

doi:10.1109/LICS52264.2021.9470690

Alignment Completeness for Relational Hoare Logics

Ramana Nagasamudram, David A. Naumann

Department of Computer Science

Stevens Institute of Technology

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

5 Scopus citations

Abstract

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.

Original language	English
Title of host publication	2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021
ISBN (Electronic)	9781665448956
DOIs	https://doi.org/10.1109/LICS52264.2021.9470690
State	Published - 29 Jun 2021
Event	36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 - Virtual, Online Duration: 29 Jun 2021 → 2 Jul 2021

Publication series

Name	Proceedings - Symposium on Logic in Computer Science
Volume	2021-June
ISSN (Print)	1043-6871

Conference

Conference	36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021
City	Virtual, Online
Period	29/06/21 → 2/07/21

Access to Document

10.1109/LICS52264.2021.9470690

Cite this

@inproceedings{0501f61d6c464fd2b4fe3d3cb6ccdfff,

title = "Alignment Completeness for Relational Hoare Logics",

abstract = "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.",

author = "Ramana Nagasamudram and Naumann, {David A.}",

note = "Publisher Copyright: {\textcopyright} 2021 IEEE.; 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 ; Conference date: 29-06-2021 Through 02-07-2021",

year = "2021",

month = jun,

day = "29",

doi = "10.1109/LICS52264.2021.9470690",

language = "English",

series = "Proceedings - Symposium on Logic in Computer Science",

booktitle = "2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021",

}

Nagasamudram, R & Naumann, DA 2021, Alignment Completeness for Relational Hoare Logics. in 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021., 9470690, Proceedings - Symposium on Logic in Computer Science, vol. 2021-June, 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Virtual, Online, 29/06/21. https://doi.org/10.1109/LICS52264.2021.9470690

TY - GEN

T1 - Alignment Completeness for Relational Hoare Logics

AU - Nagasamudram, Ramana

AU - Naumann, David A.

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 - http://www.scopus.com/inward/record.url?scp=85110491842&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85110491842&partnerID=8YFLogxK

U2 - 10.1109/LICS52264.2021.9470690

DO - 10.1109/LICS52264.2021.9470690

M3 - Conference contribution

AN - SCOPUS:85110491842

T3 - Proceedings - Symposium on Logic in Computer Science

BT - 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021

T2 - 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021

Y2 - 29 June 2021 through 2 July 2021

ER -

Alignment Completeness for Relational Hoare Logics

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this