Paper Info
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.
Year
Venue
Field
2017
NFM
Logical consequence,Separation logic,Abstraction,Programming language,Computer science,Satisfiability,Automaton,Heap (data structure),Solver,Modular design
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
13
4
Name
Order
Citations
PageRank
Constantin Enea124926.95
Ondřej Lengál2279.58
Mihaela Sighireanu365837.99
Tomás Vojnar413627.58