Alignment complete relational Hoare logics for some and all

DOI10.46298/LMCS-21(4:21)2025MaRDI QIDQ6858432zbMATH OpenFDO

Authors Ramana Nagasamudram, Anindya Banerjee, David A. Naumann

Publication date 13 February 2026

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/LMCS-21(4:21)2025

zbMATH Keywords

inductive assertion methodlogics of programsrelational Hoare logicrelational propertiesrelative completenesssemantic completeness

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• A temporal logic for asynchronous hyperproperties
• Alignment completeness for relational Hoare logics
• Automated hypersafety verification
• Beyond 2-safety: asymmetric product programs for relational program verification
• Computer aided verification. 34th international conference, CAV 2022, Haifa, Israel, August 7--10, 2022. Proceedings. Part I
• Constraint-based relational verification
• Countable nondeterminism and random assignment
• Coupling proofs are probabilistic product programs
• Data Refinement
• Exploiting synchrony and symmetry in relational verification
• Fifty years of Hoare's logic
• Hoare logic and auxiliary variables
• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 1086671 (Why is no real title available?)
• scientific article; zbMATH DE number 1948157 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• scientific article; zbMATH DE number 3351184 (Why is no real title available?)
• Inference rules for proving the equivalence of recursive procedures
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• KAT + B!
• Modular product programs
• Normal form approach to compiler design
• On Hoare logic and Kleene algebra with tests
• On the completeness of propositional Hoare logic
• Product properties and their direct verification
• Property directed self composition
• Regression verification for unbalanced recursive functions
• Relational decomposition
• Relational logic with framing and hypotheses
• Relational separation logic
• ReLoC: a mechanised relational logic for fine-grained concurrency
• RHLE: modular deductive verification of relational \(\forall \exists\) properties
• Secure information flow by self-composition
• Simple relational correctness proofs for static analyses and program transformations
• Software Verification of Hyperproperties Beyond k-Safety
• Some Properties of Predicate Transformers
• Soundness and Completeness of an Axiom System for Program Verification
• Static Analysis
• Term Rewriting and All That
• The spirit of ghost code
• Tools and Algorithms for the Construction and Analysis of Systems
• Towards modularly comparing programs using automated theorem provers
• Verification of sequential and concurrent programs
• VST-Floyd: a separation logic tool to verify correctness of C programs

This page was built for publication: Alignment complete relational Hoare logics for some and all

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