Relational separation logic

DOI10.1016/j.tcs.2006.12.036zbMath1111.68078OpenAlexW2115974895MaRDI QIDQ879369

Hongseok Yang

Publication date: 11 May 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.12.036

zbMATH Keywords

separation logicprogram verificationSchorr-Waite graph marking algorithmrelational reasoning

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Product programs and relational program logics, Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification, Blaming the client: on data refinement in the presence of pointers, Observational purity and encapsulation, Operationally-based program equivalence proofs using LCTRSs, Is Your Software on Dope?, A Higher-Order Logic for Concurrent Termination-Preserving Refinement, Modular Verification of Procedure Equivalence in the Presence of Memory Allocation, Explanation of two non-blocking shared-variable communication algorithms, Decomposing data structure commutativity proofs with \(mn\)-differencing, Relational bytecode correlations, Relational Decomposition, Inter-program Properties, A Machine-Checked Framework for Relational Separation Logic, Secure information flow by self-composition, Unnamed Item

Cites Work

• Prespecification in data refinement
• A single complete rule for data refinement
• Simple relational correctness proofs for static analyses and program transformations
• Local reasoning about a copying garbage collector
• The Logic of Bunched Implications
• BI as an assertion language for mutable data structures
• Computer Aided Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item