Detail publikace

SPEN: A Solver for Separation Logic

LENGÁL, O. VOJNAR, T. ENEA, C. SIGHIREANU, M.

Originální název

SPEN: A Solver for Separation Logic

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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

Autoři

LENGÁL, O.; VOJNAR, T.; ENEA, C.; SIGHIREANU, M.

Vydáno

9. 3. 2017

Nakladatel

Springer Verlag

Místo

Heidelberg

ISBN

978-3-319-57287-1

Kniha

Proceedings of NFM'17

Edice

Lecture Notes in Computer Science

Strany od

302

Strany do

309

Strany počet

8

URL

https://www.fit.vut.cz/research/publication/11366/

BibTex

@inproceedings{BUT135904,
  author="Ondřej {Lengál} and Tomáš {Vojnar} and Constantin {Enea} and Mihaela {Sighireanu}",
  title="SPEN: A Solver for Separation Logic",
  booktitle="Proceedings of NFM'17",
  year="2017",
  series="Lecture Notes in Computer Science",
  volume="10227",
  pages="302--309",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-319-57288-8\{_}22",
  isbn="978-3-319-57287-1",
  url="https://www.fit.vut.cz/research/publication/11366/"
}