Detail výsledku

Compositional Entailment Checking for a Fragment of Separation Logic

ENEA, C.; LENGÁL, O.; SIGHIREANU, M.; VOJNAR, T. Compositional Entailment Checking for a Fragment of Separation Logic. In Proceedings of APLAS'14. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2014. p. 314-333. ISBN: 978-3-319-12735-4.
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Enea Constantin
Lengál Ondřej, doc. Ing., Ph.D., FIT (FIT)
Sighireanu Mihaela, prof. Ing., PhD.
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Abstrakt

We present a (semi-)decision procedure for checking entailment between separation logic formulas with inductive predicates specifying complex data structures corresponding to finite nesting of various kinds of linked lists: acyclic or cyclic, singly or doubly linked, skip lists, etc. The decision procedure is compositional in the sense that it reduces the problem of checking entailment between two arbitrary formulas to the problem of checking entailment between a formula and an atom. Subsequently, in case the atom is a predicate, we reduce the entailment to testing membership of a tree derived from the formula in the language of a tree automaton derived from the predicate. We implemented this decision procedure and tested it successfully on verification conditions obtained from programs using singly and doubly linked nested lists as well as skip lists.

Klíčová slova


program verification, decision procedures, separation logic, tree automata

Rok
2014
Strany
314–333
Sborník
Proceedings of APLAS'14
Řada
Lecture Notes in Computer Science
Svazek
8858
Konference
12th Asian Symposium on Programming Languages and Systems -- APLAS'14
ISBN
978-3-319-12735-4
Vydavatel
Springer Verlag
Místo
Heidelberg
EID Scopus
2-s2.0-84910017407
BibTeX 
@inproceedings{BUT111608,
  author="Constantin {Enea} and Ondřej {Lengál} and Mihaela {Sighireanu} and Tomáš {Vojnar}",
  title="Compositional Entailment Checking for a Fragment of Separation Logic",
  booktitle="Proceedings of APLAS'14",
  year="2014",
  series="Lecture Notes in Computer Science",
  volume="8858",
  pages="314--333",
  publisher="Springer Verlag",
  address="Heidelberg",
  isbn="978-3-319-12735-4"
}
Projekty
Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí, GAČR, Standardní projekty, GA14-11384S, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, zahájení: 2011-01-01, ukončení: 2015-12-31, ukončen
Spolehlivost a bezpečnost v IT, VUT, Vnitřní projekty VUT, FIT-S-14-2486, zahájení: 2014-01-01, ukončení: 2016-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