Conference paperENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. SPEN: A Solver for Separation Logic. In: Proceedings of NFM'17. Heidelberg: Springer Verlag, 2017, pp. 302309. ISBN 9783319572871.  Publication language:  english 

Original title:  SPEN: A Solver for Separation Logic 

Title (cs):  SPEN: Solver pro separační logiku 

Pages:  302309 

Proceedings:  Proceedings of NFM'17 

Conference:  NASA Formal Methods 2017 

Series:  LNCS 10227 

Place:  Heidelberg, DE 

Year:  2017 

ISBN:  9783319572871 

DOI:  10.1007/9783319572888_22 

Publisher:  Springer Verlag 

Keywords 

separation logic entailment checking satisfiability checking SMT solving SAT solving tree automata tool support 
Annotation 

SPEN is a solver for a fragment of separation logic (SL) with inductivelydefined predicates covering both (nested) list structures as well as various kinds of trees, possibly extended with data. The main functionalities of SPEN are deciding the satisfiability of a formula and the validity of an entailment between two formulas, which are essential for verification of heap manipulating programs. The solver also provides models for satisfiable formulas and diagnosis for invalid entailments. SPEN combines several concepts in a modular way, such as boolean abstractions of SL formulas, SAT and SMT solving, and tree automata membership testing. The solver has been successfully applied to a ratherlarge benchmark of various problems issued from program verification too. 
BibTeX: 

@INPROCEEDINGS{
author = {Constantin Enea and Ond{\v{r}}ej Leng{\'{a}}l and
Mihaela Sighireanu and Tom{\'{a}}{\v{s}} Vojnar},
title = {SPEN: A Solver for Separation Logic},
pages = {302309},
booktitle = {Proceedings of NFM'17},
series = {LNCS 10227},
year = {2017},
location = {Heidelberg, DE},
publisher = {Springer Verlag},
ISBN = {9783319572871},
doi = {10.1007/9783319572888_22},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php.en.iso88592?id=11366}
} 
