Detail výsledku

SPEN: A Solver for Separation Logic

LENGÁL, O.; VOJNAR, T.; ENEA, C.; SIGHIREANU, M. SPEN: A Solver for Separation Logic. In Proceedings of NFM'17. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017. p. 302-309. ISBN: 978-3-319-57287-1.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Lengál Ondřej, doc. Ing., Ph.D., UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Enea Constantin, FIT (FIT)
Sighireanu Mihaela, prof. Ing., PhD.
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

Rok
2017
Strany
302–309
Sborník
Proceedings of NFM'17
Řada
Lecture Notes in Computer Science
Svazek
10227
Konference
NASA Formal Methods 2017
ISBN
978-3-319-57287-1
Vydavatel
Springer Verlag
Místo
Heidelberg
DOI
10.1007/978-3-319-57288-8_22
UT WoS
000890067500022
EID Scopus
2-s2.0-85018662996
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/"
}
Soubory
Projekty
Bezpečné a spolehlivé počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-17-4014, zahájení: 2017-03-01, ukončení: 2020-02-29, ukončen
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, zahájení: 2016-01-01, ukončení: 2020-12-31, ukončen
ROBUST - Verifikace a hledání chyb v pokročilém softwaru, GAČR, Standardní projekty, GA17-12465S, zahájení: 2017-01-01, ukončení: 2019-12-31, ukončen
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru