Conference paper

ENEA 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. 302-309. ISSN 0302-9743.
Publication language:english
Original title:SPEN: A Solver for Separation Logic
Title (cs):SPEN: Solver pro separační logiku
Pages:302-309
Proceedings:Proceedings of NFM'17
Conference:NASA Formal Methods 2017
Series:LNCS 10227
Place:Heidelberg, DE
Year:2017
Journal:Lecture Notes in Computer Science, No. 10227, DE
ISSN:0302-9743
Publisher:Springer Verlag
Files: 
+Type Name Title +Size Last modified
iconspen.pdf308 KB2017-05-09 10:07:27
^ Select all
With selected:
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 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.
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 = {302--309},
   booktitle = {Proceedings of NFM'17},
   series = {LNCS 10227},
   journal = {Lecture Notes in Computer Science},
   number = {10227},
   year = {2017},
   location = {Heidelberg, DE},
   publisher = {Springer Verlag},
   ISSN = {0302-9743},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.en.iso-8859-2?id=11366}
}

Your IPv4 address: 54.198.221.13
Switch to IPv6 connection

DNSSEC [dnssec]