A theorem prover for Boolean BI

DOI10.1145/2429069.2429095zbMath1301.68221OpenAlexW2085320115MaRDI QIDQ2931798

Jong Hyun Park, Jeongbong Seo, Sungwoo Park

Publication date: 27 November 2014

Published in: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.259.8072

zbMATH Keywords

separation logictheorem provernested sequent calculusBoolean bunched implications

Mathematics Subject Classification ID

Related Items (3)

Completeness for a First-Order Abstract Separation Logic ⋮ Proof tactics for assertions in separation logic ⋮ Unnamed Item

Uses Software

• VeriFast
• jStar

This page was built for publication: A theorem prover for Boolean BI