Compositional Entailment Checking for a Fragment of Separation Logic

DOI10.1007/978-3-319-12736-1_17zbMath1453.68046OpenAlexW3023397123MaRDI QIDQ2789053

Mihaela Sighireanu, Tomáš Vojnar, Constantin Enea, Ondřej Lengál

Publication date: 26 February 2016

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-12736-1_17

Mathematics Subject Classification ID

Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Decision Procedure for Entailment of Symbolic Heaps with Arrays, Automated mutual induction proof in separation logic, Unnamed Item, Compositional entailment checking for a fragment of separation logic, Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic, Unnamed Item, A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints