Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and History

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

6 Scopus citations

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.

Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation
Subtitle of host publicationEngineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings
EditorsTiziana Margaria, Bernhard Steffen
Pages93-116
Number of pages24
DOIs
StatePublished - 2020
Event9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020 - Rhodes, Greece
Duration: 20 Oct 202030 Oct 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12477 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020
Country/TerritoryGreece
CityRhodes
Period20/10/2030/10/20

Fingerprint

Dive into the research topics of 'Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and History'. Together they form a unique fingerprint.

Cite this