Detail výsledku

Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution)

DUDKA, K.; PERINGER, P.; VOJNAR, T. Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2014. p. 412-414. ISBN: 978-3-642-54861-1.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Dudka Kamil, Ing.
Peringer Petr, Dr. Ing., UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Abstrakt

Predator is a shape analyzer that uses the abstract domain of symbolicmemory graphs in order to support various forms of low-level memory manipulation commonly used in optimized C code. This paper briefly describes the verification approach taken by Predator and its strengths and weaknesses revealed during its participation in the Software Verification Competition (SV-COMP14).

Klíčová slova


dynamic linked data structures
separation logic
symbolic memory graphs
list manipulation
low-level memory manipulation
memory safety
shape analysis

URL
Rok
2014
Strany
412–414
Sborník
Tools and Algorithms for the Construction and Analysis of Systems
Řada
Lecture Notes in Computer Science
Svazek
8413
Konference
European Joint Conferences on Theory and Practice of Software -- ETAPS'14 (TACAS'14)
ISBN
978-3-642-54861-1
Vydavatel
Springer Verlag
Místo
Heidelberg
DOI
10.1007/978-3-642-54862-8_33
EID Scopus
2-s2.0-84900537246
BibTeX 
@inproceedings{BUT111526,
  author="Kamil {Dudka} and Petr {Peringer} and Tomáš {Vojnar}",
  title="Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution)",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  year="2014",
  series="Lecture Notes in Computer Science",
  volume="8413",
  pages="412--414",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-642-54862-8\{_}33",
  isbn="978-3-642-54861-1",
  url="http://link.springer.com/chapter/10.1007/978-3-642-54862-8_33"
}
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