RHLE: modular deductive verification of relational \(\forall \exists\) properties
From MaRDI portal
Publication:6176567
DOI10.1007/978-3-031-21037-2_4zbMath1524.68082arXiv2002.02904OpenAlexW3107663325MaRDI QIDQ6176567
Qianchuan Ye, Michael K. Zhang, Unnamed Author, 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
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Unnamed Item
- The existence of refinement mappings
- Constraint-based relational verification
- Resources, concurrency, and local reasoning
- Verified Software Toolchain
- Reverse Hoare Logic
- Secure information flow by self-composition
- Simple relational correctness proofs for static analyses and program transformations
- Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification
- Formal certification of code-based cryptographic proofs
- Synthesis of Circular Compositional Program Proofs via Abduction
- An axiomatic basis for computer programming
- Static Analysis
