Proof search for propositional abstract separation logics via labelled sequents

DOI10.1145/2535838.2535864zbMath1284.68402arXiv1307.5592OpenAlexW2118029706MaRDI QIDQ5408442

Zhé Hóu, Ranald Clouston, Rajeev Goré, Alwen Tiu

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://arxiv.org/abs/1307.5592

zbMATH Keywords

automated reasoningbunched implicationslabelled sequentscounter-model constructionabstract separation logic

Mathematics Subject Classification ID

Related Items (5)

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction ⋮ 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 ⋮ Proof tactics for assertions in separation logic

Uses Software

• Pesca

This page was built for publication: Proof search for propositional abstract separation logics via labelled sequents