RHLE: modular deductive verification of relational properties

DOI10.1007/978-3-031-21037-2_4zbMATH Open1524.68082arXiv2002.02904OpenAlexW3107663325MaRDI QIDQ6176567FDOQ6176567

Authors: Qianchuan Ye, Michael K. Zhang, Benjamin Delaware 

Publication date: 25 July 2023

Published in: Programming Languages and Systems (Search for Journal in Brave)

Abstract: Hoare-style program logics are a popular and effective technique for software verification. Relational program logics are an instance of this approach that enables reasoning about relationships between the execution of two or more programs. Existing relational program logics have focused on verifying that all runs of a collection of programs do not violate a specified relational behavior. Several important relational properties, including refinement and noninterference, do not fit into this category, as they also mandate the existence of specific desirable executions. This paper presents RHLE, a logic for verifying these sorts of relational $forallexists$ properties. Key to our approach is a novel form of function specification that employs a variant of ghost variables to ensure that valid implementations exhibit certain behaviors. We have used a program verifier based on RHLE to verify a diverse set of relational $forallexists$ properties drawn from the literature.

Full work available at URL: https://arxiv.org/abs/2002.02904

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Cites Work

• Formal certification of code-based cryptographic proofs
• Title not available (Why is that?)
• The existence of refinement mappings
• An axiomatic basis for computer programming
• Resources, concurrency, and local reasoning
• Verified software toolchain (invited talk)
• Synthesis of circular compositional program proofs via abduction
• Secure information flow by self-composition
• Simple relational correctness proofs for static analyses and program transformations
• Static Analysis
• Beyond 2-safety: asymmetric product programs for relational program verification
• Constraint-based relational verification
• Reverse Hoare logic

This page was built for publication: RHLE: modular deductive verification of relational \(\forall \exists\) properties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6176567)