Conference paperENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. In: Proceedings of APLAS'14. Heidelberg: Springer Verlag, 2014, pp. 314333. ISBN 9783319127354.  Publication language:  english 

Original title:  Compositional Entailment Checking for a Fragment of Separation Logic 

Title (cs):  Kompozitní testování implikace pro fragment separační logiky 

Pages:  314333 

Proceedings:  Proceedings of APLAS'14 

Conference:  12th Asian Symposium on Programming Languages and Systems  APLAS'14 

Series:  LNCS 8858 

Place:  Heidelberg, DE 

Year:  2014 

ISBN:  9783319127354 

Publisher:  Springer Verlag 

Keywords 

program verification, decision procedures, separation logic, tree automata 
Annotation 

We present a (semi)decision procedure for checking entailment between
separation logic formulas with inductive predicates specifying complex
data structures corresponding to finite nesting of various kinds of
linked lists: acyclic or cyclic, singly or doubly linked, skip lists,
etc. The decision procedure is compositional in the sense that it
reduces the problem of checking entailment between two arbitrary
formulas to the problem of checking entailment between a formula and an
atom. Subsequently, in case the atom is a predicate, we reduce the
entailment to testing membership of a tree derived from the formula in
the language of a tree automaton derived from the predicate. We
implemented this decision procedure and tested it successfully on
verification conditions obtained from programs using singly and doubly
linked nested lists as well as skip lists. 
BibTeX: 

@INPROCEEDINGS{
author = {Constantin Enea and Ond{\v{r}}ej Leng{\'{a}}l and Mihaela
Sighireanu and Tom{\'{a}}{\v{s}} Vojnar},
title = {Compositional Entailment Checking for a Fragment of
Separation Logic},
pages = {314333},
booktitle = {Proceedings of APLAS'14},
series = {LNCS 8858},
year = {2014},
location = {Heidelberg, DE},
publisher = {Springer Verlag},
ISBN = {9783319127354},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=10701}
} 
