@inproceedings{8925af5286e74f75b49bc1d951ee8334,
title = "SPEN: A solver for separation logic",
abstract = "Spen is a solver for a fragment of separation logic (SL) with inductively-defined 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 rather large benchmark of various problems issued from program verification tools.",
author = "Constantin Enea and Ond{\v r}ej Leng{\'a}l and Mihaela Sighireanu and Tom{\'a}{\v s} Vojnar",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 9th International Symposium on NASA Formal Methods, NFM 2017 ; Conference date: 16-05-2017 Through 18-05-2017",
year = "2017",
month = jan,
day = "1",
doi = "10.1007/978-3-319-57288-8\_22",
language = "English",
isbn = "9783319572871",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "302--309",
editor = "Misty Davies and Temesghen Kahsai and Clark Barrett",
booktitle = "NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings",
}