A proof system for separation logic with magic wand

DOI10.1145/2535838.2535871zbMath1284.68408OpenAlexW2144482530WikidataQ130864090 ScholiaQ130864090MaRDI QIDQ5408443

Won-Yeol Lee, Sungwoo Park

Publication date: 10 April 2014

Published in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2535838.2535871

zbMATH Keywords

proof systemseparation logictheorem prover

Mathematics Subject Classification ID

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

Related Items (8)

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction ⋮ Symbolic execution proofs for higher order store programs ⋮ Automated Theorem Proving for Assertions in Separation Logic with All Connectives ⋮ Completeness for a First-Order Abstract Separation Logic ⋮ Separation logics and modalities: a survey ⋮ Sound Automation of Magic Wands ⋮ An adaptation-complete proof system for local reasoning about cloud storage systems ⋮ Reasoning about block-based cloud storage systems via separation logic

Uses Software

• Smallfoot
• jStar

This page was built for publication: A proof system for separation logic with magic wand