Detail publikace

Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution)

DUDKA, K.; MÜLLER, P.; PERINGER, P.; VOJNAR, T. Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Lecture Notes in Computer Science Volume 7795. Berlin: Springer Verlag, 2013. p. 627-629. ISBN: 978-3-642-36742-7. ISSN: 0302-9743.
Název česky
Predator: Nástroj pro verifikaci nízkoúrovňové manipulace seznamů (soutěžní příspěvek)
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Dudka Kamil, Ing.
Müller Petr, Ing.
Peringer Petr, Dr. Ing. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
URL
Klíčová slova

dynamic linked data structuresseparation logic symbolic memory graphslist manipulationlow-level memory manipulationmemory safetyshape analysis

Abstrakt

Predator je nástroj pro automatickou formální verifikaci sekvenčních C programů, které pracují s ukazateli a vázanými seznamy. Základní algoritmy nástroje Predator byly původně inspirovány pracemi založenými na separační logice se seznamovými predikáty vyššího řádu, ale teď jsou založené výhradně na grafech a značně rozšířené o podporu různých podob nízkoúrovňové práce s pamětí používané v systémovém kódu. Tento článek stručně uvádí nástroj Predator a popisuje jeho účast v mezinárodní soutěži SV-COMP'13 pořádané na konferenci TACAS'13.

Rok
2013
Strany
627–629
Časopis
Lecture Notes in Computer Science, roč. 2013, č. 7795, ISSN 0302-9743
Sborník
Tools and Algorithms for the Construction and Analysis of Systems
Řada
Lecture Notes in Computer Science Volume 7795
ISBN
978-3-642-36742-7
Vydavatel
Springer Verlag
Místo
Berlin
BibTeX 
@inproceedings{BUT103454,
  author="Kamil {Dudka} and Petr {Müller} and Petr {Peringer} and Tomáš {Vojnar}",
  title="Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution)",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  year="2013",
  series="Lecture Notes in Computer Science Volume 7795",
  journal="Lecture Notes in Computer Science",
  volume="2013",
  number="7795",
  pages="627--629",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-642-36742-7",
  issn="0302-9743",
  url="http://link.springer.com/chapter/10.1007/978-3-642-36742-7_49"
}
Nahoru