Detail publikace

Deciding Entailments in Inductive Separation Logic with Tree Automata

ROGALEWICZ, A.; VOJNAR, T.; IOSIF, R. Deciding Entailments in Inductive Separation Logic with Tree Automata. In Proceedings of ATVA'14. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2014. p. 201-218. ISBN: 978-3-319-11935-9.
Název česky
Rozhodovací procedura pro separační logiku s induktivními definicemi založená na stromových automatech
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Radu Iosif
URL
Klíčová slova

Separation logic, entailment, decision procedure, tree automata, EXPTIME-complete

Abstrakt

Článek popisuje rozhodovací proceduru pro fragment separační logiky s induktivními definicemi. Rozhodovací procedura je založená na polynomiální redukci na problém incluze jazyků stromových automatů. Tato rozhodovací procedura je EXPTIME-úplná.

Rok
2014
Strany
201–218
Sborník
Proceedings of ATVA'14
Řada
Lecture Notes in Computer Science
Svazek
8837
Konference
12th International Symposium on Automated Technology for Verification and Analysis, Sydney, AU
ISBN
978-3-319-11935-9
Vydavatel
Springer Verlag
Místo
Heidelberg
UT WoS
000345585700019
EID Scopus
2-s2.0-84908681084
BibTeX 
@inproceedings{BUT111633,
  author="Adam {Rogalewicz} and Tomáš {Vojnar} and Iosif {Radu}",
  title="Deciding Entailments in Inductive Separation Logic with Tree Automata",
  booktitle="Proceedings of ATVA'14",
  year="2014",
  series="Lecture Notes in Computer Science",
  volume="8837",
  pages="201--218",
  publisher="Springer Verlag",
  address="Heidelberg",
  isbn="978-3-319-11935-9",
  url="http://rd.springer.com/chapter/10.1007%2F978-3-319-11936-6_15"
}
Nahoru