Publication Details

SPEN: A Solver for Separation Logic

ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. SPEN: A Solver for Separation Logic. In: Proceedings of NFM'17. Lecture Notes in Computer Science, vol. 10227. Heidelberg: Springer Verlag, 2017, pp. 302-309. ISBN 978-3-319-57287-1.
Czech title
SPEN: Solver pro separační logiku
Type
conference paper
Language
english
Authors
Enea Constantin (LIAFA UP7/CNRS)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Sighireanu Mihaela (LIAFA UP7/CNRS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Keywords


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

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 ratherlarge benchmark of various problems issued from program verification too.

Published
2017
Pages
302-309
Proceedings
Proceedings of NFM'17
Series
Lecture Notes in Computer Science
Volume
10227
Conference
NASA Formal Methods 2017, Moffett Field, US
ISBN
978-3-319-57287-1
Publisher
Springer Verlag
Place
Heidelberg, DE
DOI
10.1007/978-3-319-57288-8_22
UT WoS
000890067500022
EID Scopus
2-s2.0-85018662996
BibTeX 
@INPROCEEDINGS{FITPUB11366,
   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 = "302--309",
   booktitle = "Proceedings of NFM'17",
   series = "Lecture Notes in Computer Science",
   volume = 10227,
   year = 2017,
   location = "Heidelberg, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-319-57287-1",
   doi = "10.1007/978-3-319-57288-8\_22",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11366"
}
Back to top