Detail výsledku

Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark (Competition Contribution)

KOTOUN, M.; PERINGER, P.; ŠOKOVÁ, V.; VOJNAR, T. Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark (Competition Contribution). In Proceedings of TACAS 2016. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2016. p. 942-945. ISBN: 978-3-662-49673-2.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Kotoun Michal, Ing.
Peringer Petr, Dr. Ing., UITS (FIT)
Šoková Veronika, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Abstrakt

This paper describes shortly the PredatorHP (Predator Hunting Party) analyzer and its participation in the SV-COMP 2016 software verification competition. The paper starts by a brief sketch of the Predator shape analyzer on which PredatorHP is built, using multiple, concurrently running, specialised instances of Predator. The paper explains why the concrete mix of the different Predators was used, based on some characteristics of the SV-COMP  benchmark.

Klíčová slova

formal verification, program analysis, shape analysis, symbolic memory graphs, bug hunting, memory safety, software verification competition

URL
Rok
2016
Strany
942–945
Sborník
Proceedings of TACAS 2016
Řada
Lecture Notes in Computer Science
Svazek
9636
Konference
European Joint Conferences on Theory and Practice of Software -- ETAPS'16 (TACAS'16)
ISBN
978-3-662-49673-2
Vydavatel
Springer Verlag
Místo
Heidelberg
DOI
10.1007/978-3-662-49674-9_66
UT WoS
000406428000066
EID Scopus
2-s2.0-84964056792
BibTeX 
@inproceedings{BUT130970,
  author="Michal {Kotoun} and Petr {Peringer} and Veronika {Šoková} and Tomáš {Vojnar}",
  title="Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark (Competition Contribution)",
  booktitle="Proceedings of TACAS 2016",
  year="2016",
  series="Lecture Notes in Computer Science",
  volume="9636",
  pages="942--945",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-662-49674-9\{_}66",
  isbn="978-3-662-49673-2",
  url="http://link.springer.com/chapter/10.1007%2F978-3-662-49674-9_66"
}
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
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru