Relational logic with framing and hypotheses

DOI10.4230/LIPICS.FSTTCS.2016.11MaRDI QIDQ4636558zbMATH OpenFDO

Authors Anindya Banerjee, David A. Naumann, Mohammad Nikouei

Publication date 19 April 2018

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

zbMATH Keywords

program equivalenceframe conditionsrelational Hoare logicproduct programsregion logic

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Relational separation logic
• Product programs and relational program logics
• A machine-checked framework for relational separation logic
• Relational decomposition
• Publication:3204444

Cited in

(16)

• Modular verification of procedure equivalence in the presence of memory allocation
• Product programs and relational program logics
• Decomposing data structure commutativity proofs with \(mn\)-differencing
• Beyond 2-safety: asymmetric product programs for relational program verification
• Operationally-based program equivalence proofs using LCTRSs
• Assertion and hypothesis: a logical framework for their opposition relations:
• RHLE: modular deductive verification of relational \(\forall \exists\) properties
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• Relational verification via invariant-guided synchronization
• Predicate pairing with abstraction for relational verification
• Relational separation logic
• scientific article; zbMATH DE number 3854395 (Why is no real title available?)
• Relational decomposition
• A machine-checked framework for relational separation logic
• A first-order logic with frames
• Relational program reasoning using compiler IR

This page was built for publication: Relational logic with framing and hypotheses

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