On Automated Lemma Generation for Separation Logic with Inductive Definitions

DOI10.1007/978-3-319-24953-7_7zbMath1471.68139arXiv1507.05581OpenAlexW1267783697MaRDI QIDQ3460548

Constantin Enea, Mihaela Sighireanu, Zhilin Wu

Publication date: 8 January 2016

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1507.05581

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (5)

Automated mutual induction proof in separation logic ⋮ Compositional entailment checking for a fragment of separation logic ⋮ An efficient cyclic entailment procedure in a fragment of separation logic ⋮ Unnamed Item ⋮ A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints

This page was built for publication: On Automated Lemma Generation for Separation Logic with Inductive Definitions