RHLE: modular deductive verification of relational properties

DOI10.1007/978-3-031-21037-2_4MaRDI QIDQ6176567zbMATHOpenAlexFDO

Authors Qianchuan Ye, Michael K. Zhang, Benjamin Delaware

Publication date 25 July 2023

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

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)

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.

Recommendations

• Relational logic with framing and hypotheses
• Product programs and relational program logics
• Certified verification of relational properties
• Beyond 2-safety: asymmetric product programs for relational program verification
• Relational verification through Horn clause transformation

Cites work

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

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)