Publication detail

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

KOTOUN, M. PERINGER, P. ŠOKOVÁ, V. VOJNAR, T.

Original Title

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

Type

conference paper

Language

English

Original Abstract

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.

Keywords

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

Authors

KOTOUN, M.; PERINGER, P.; ŠOKOVÁ, V.; VOJNAR, T.

Released

2. 4. 2016

Publisher

Springer Verlag

Location

Heidelberg

ISBN

978-3-662-49673-2

Book

Proceedings of TACAS 2016

Edition

Lecture Notes in Computer Science

Pages from

942

Pages to

945

Pages count

4

URL

http://link.springer.com/chapter/10.1007%2F978-3-662-49674-9_66

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"
}