Separation logic adapted for proofs by rewriting

DOI10.1007/978-3-642-14052-5_34MaRDI QIDQ5747672zbMATH OpenOpenAlexFDO

Authors Magnus O. Myreen

Publication date 14 September 2010

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14052-5_34

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Computer Science Logic
• Automated theorem proving for assertions in separation logic with all connectives
• Proof tactics for assertions in separation logic
• Automated cyclic entailment proofs in separation logic
• A proof system for separation logic with magic wand

Cited in

(7)

• Proof tactics for assertions in separation logic
• A machine-checked framework for relational separation logic
• Cyclic proofs of program termination in separation logic
• Automated theorem proving for assertions in separation logic with all connectives
• Lightweight Separation
• A complete axiomatisation for quantifier-free separation logic
• Ribbon proofs for separation logic

Describes a project that uses

Uses Software

• ACL2
• HOL

This page was built for publication: Separation logic adapted for proofs by rewriting

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