Publication detail

Predator Hunting Party (Competition Contribution)

PERINGER, P. MÜLLER, P. VOJNAR, T.

Original Title

Predator Hunting Party (Competition Contribution)

Type

conference paper

Language

English

Original Abstract

This paper introduces PredatorHP (Predator Hunting Party), a program verifier built on top of the Predator shape analyser, and discusses its participation in the SV-COMP'15 software verification competition. Predator is a sound shape analyser dealing with C programs with lists implemented via low-level pointer operations. PredatorHP uses Predator to prove programs safe while at the same time using several bounded versions of Predator for bug hunting.

Keywords

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

Authors

PERINGER, P.; MÜLLER, P.; VOJNAR, T.

RIV year

2015

Released

13. 4. 2015

Publisher

Springer Verlag

Location

Heidelberg

ISBN

978-3-662-46680-3

Book

Proceedings of TACAS'15

Edition

Lecture Notes in Computer Science

Pages from

443

Pages to

446

Pages count

4

URL

http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_40

BibTex

@inproceedings{BUT119878,
  author="Petr {Peringer} and Petr {Müller} and Tomáš {Vojnar}",
  title="Predator Hunting Party (Competition Contribution)",
  booktitle="Proceedings of TACAS'15",
  year="2015",
  series="Lecture Notes in Computer Science",
  volume="9035",
  pages="443--446",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-662-46681-0\{_}40",
  isbn="978-3-662-46680-3",
  url="http://link.springer.com/chapter/10.1007%2F978-3-662-46681-0_40"
}