References & Citations
Computer Science > Logic in Computer Science
Title: Thirty-seven years of relational Hoare logic: remarks on its principles and history
(Submitted on 13 Jul 2020 (v1), last revised 16 Jul 2022 (this version, v6))
Abstract: 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.
Submission history
From: David Naumann [view email][v1] Mon, 13 Jul 2020 14:53:22 GMT (46kb)
[v2] Sun, 19 Jul 2020 22:25:19 GMT (46kb)
[v3] Mon, 3 Aug 2020 16:07:12 GMT (47kb)
[v4] Fri, 29 Jan 2021 02:19:59 GMT (48kb)
[v5] Thu, 3 Jun 2021 14:48:32 GMT (47kb)
[v6] Sat, 16 Jul 2022 01:52:24 GMT (47kb)
Link back to: arXiv, form interface, contact.