Extended transitive separation logic

DOI10.1016/j.jlamp.2014.12.002zbMath1330.03071MaRDI QIDQ2347905

Bernhard Möller, Han-Hing Dang

Publication date: 10 June 2015

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2014.12.002

zbMATH Keywords

verification; reachability; separation logic; sharing; strong separation

Mathematics Subject Classification ID

03B70: Logic in computer science

03G25: Other algebras related to logic

68P05: Data structures

Uses Software

• TPTP
• Prover9
• Mace4
• Z

Cites Work

• Algebraic separation logic
• Towards pointer algebra
• The inverse semigroup of a sum-ordered semiring
• Extending separation logic with fixpoints and postponed substitution
• The TPTP problem library. CNF release v1. 2. 1
• A completeness theorem for Kleene algebras and the algebra of regular events
• Characterizing determinacy in Kleene algebras
• Calculating with acyclic and cyclic lists
• Proof of correctness of data representations
• Reverse Exchange for Concurrency and Local Reasoning
• Transitive Separation Logic
• The ramifications of sharing in data structures
• Abstraction of Object Graphs in Program Verification
• Automated Reasoning in Kleene Algebra
• Foundations of Concurrent Kleene Algebra
• Kleene algebra with domain
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Relational and Kleene-Algebraic Methods in Computer Science
• Unnamed Item
• Unnamed Item