TY - GEN
T1 - Thirty-Seven Years of Relational Hoare Logic
T2 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020
AU - Naumann, David A.
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020
Y1 - 2020
N2 - Relational Hoare logics extend the applicability of modular, deductive verification to encompass important 2-run properties including dependency requirements such as confidentiality and program relations such as equivalence or similarity between program versions. A considerable number of recent works introduce different relational Hoare logics without yet converging on a core set of proof rules. This paper looks backwards to little known early work. This brings to light some principles that clarify and organize the rules as well as suggesting a new rule and a new notion of completeness.
AB - Relational Hoare logics extend the applicability of modular, deductive verification to encompass important 2-run properties including dependency requirements such as confidentiality and program relations such as equivalence or similarity between program versions. A considerable number of recent works introduce different relational Hoare logics without yet converging on a core set of proof rules. This paper looks backwards to little known early work. This brings to light some principles that clarify and organize the rules as well as suggesting a new rule and a new notion of completeness.
UR - http://www.scopus.com/inward/record.url?scp=85096576945&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85096576945&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-61470-6_7
DO - 10.1007/978-3-030-61470-6_7
M3 - Conference contribution
AN - SCOPUS:85096576945
SN - 9783030614690
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 93
EP - 116
BT - Leveraging Applications of Formal Methods, Verification and Validation
A2 - Margaria, Tiziana
A2 - Steffen, Bernhard
Y2 - 20 October 2020 through 30 October 2020
ER -