Detail výsledku

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. no. 7795, p. 627-629. ISBN: 978-3-642-36742-7. ISSN: 0302-9743.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Dudka Kamil, Ing., UITS (FIT)
Müller Petr, Ing., UITS (FIT)
Peringer Petr, Dr. Ing., UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Abstrakt

Predator is a tool for automated formal verification of sequential C programs operating with pointers and linked lists. The core algorithms of Predator were originally inspired by works on separation logic with higher-order list predicates, but they are now purely graph-based and significantly extended to support various forms of low-level memory manipulation used in system-level code. This paper briefly introduces Predator and describes its participation in the Software Verification Competition SV-COMP'13 held at TACAS'13.

Klíčová slova
dynamic linked data structures
separation logic
symbolic memory graphs
list manipulation
low-level memory manipulation
memory safety
shape analysis
URL
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
Konference
European Joint Conferences on Theory and Practice of Software -- ETAPS'13 (TACAS'13)
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"
}
Projekty
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
Pokročilé bezpečné, spolehlivé a adaptivní IT, VUT, Vnitřní projekty VUT, FIT-S-11-1, zahájení: 2011-01-01, ukončení: 2013-12-31, ukončen
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti, GAČR, Standardní projekty, GAP103/10/0306, zahájení: 2010-01-01, ukončení: 2013-12-31, řešení
Verifikace a optimalizace počítačových systémů, VUT, Vnitřní projekty VUT, FIT-S-12-1, zahájení: 2012-01-01, ukončení: 2014-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru