A proof system for separation logic with magic wand

DOI10.1145/2535838.2535871MaRDI QIDQ5408443zbMATH OpenOpenAlexWikidataFDO

Authors 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)

Recommendations

• Computer Science Logic
• Separation Logic Tutorial
• Automated theorem proving for assertions in separation logic with all connectives
• Completeness and expressiveness of pointer program verification by separation logic
• Separation Logic for Higher-Order Store

Cited in

(17)

• Backwards and forwards with separation logic
• An adaptation-complete proof system for local reasoning about cloud storage systems
• Reasoning about block-based cloud storage systems via separation logic
• Symbolic execution proofs for higher order store programs
• Completeness for a first-order abstract separation logic
• Labelled cyclic proofs for separation logic
• Automated theorem proving for assertions in separation logic with all connectives
• Separation logics and modalities: a survey
• Structuring the verification of heap-manipulating programs
• Expressive completeness of separation logic with two variables and no separating conjunction
• Computer Science Logic
• Ribbon proofs for separation logic
• Parametric completeness for separation theories
• Proof search for propositional abstract separation logics via labelled sequents
• Separation logic adapted for proofs by rewriting
• Separation logic style reasoning in a refinement based language
• Sound Automation of Magic Wands

Describes a project that uses

Uses Software

• jStar
• Smallfoot

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

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