Publication detail

Predator Hunting Party (Competition Contribution)

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

Original Title

Predator Hunting Party (Competition Contribution)

English Title

Predator Hunting Party (Competition Contribution)

Type

conference paper

Language

en

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.

English 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

RIV year

2015

Released

13.04.2015

Publisher

Springer Verlag

Location

Heidelberg

ISBN

978-3-662-46680-3

Book

Proceedings of TACAS'15

Edition

Lecture Notes in Computer Science

Edition number

NEUVEDEN

Pages from

443

Pages to

446

Pages count

4

URL

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

Documents

BibTex 


@inproceedings{BUT119878,
  author="Petr {Peringer} and Petr {Müller} and Tomáš {Vojnar}",
  title="Predator Hunting Party (Competition Contribution)",
  annote="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.",
  address="Springer Verlag",
  booktitle="Proceedings of TACAS'15",
  chapter="119878",
  doi="10.1007/978-3-662-46681-0_40",
  edition="Lecture Notes in Computer Science",
  howpublished="print",
  institution="Springer Verlag",
  year="2015",
  month="april",
  pages="443--446",
  publisher="Springer Verlag",
  type="conference paper"
}