Publication detail

Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution)

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

Original Title

Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution)

English Title

Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution)

Type

conference paper

Language

en

Original Abstract

Predator is a tool for automated formal verification of sequential C programs operating with pointers and linked lists. The core algorithms of Predator were originally inspired by works on separation logic with higher-order list predicates, but they are now purely graph-based and significantly extended to support various forms of low-level memory manipulation used in system-level code. This paper briefly introduces Predator and describes its participation in the Software Verification Competition SV-COMP'13 held at TACAS'13.

English abstract

Predator is a tool for automated formal verification of sequential C programs operating with pointers and linked lists. The core algorithms of Predator were originally inspired by works on separation logic with higher-order list predicates, but they are now purely graph-based and significantly extended to support various forms of low-level memory manipulation used in system-level code. This paper briefly introduces Predator and describes its participation in the Software Verification Competition SV-COMP'13 held at TACAS'13.

Keywords

dynamic linked data structuresseparation logic symbolic memory graphslist manipulationlow-level memory manipulationmemory safetyshape analysis

RIV year

2013

Released

17.03.2013

Publisher

Springer Verlag

Location

Berlin

ISBN

978-3-642-36742-7

Book

Tools and Algorithms for the Construction and Analysis of Systems

Edition

Lecture Notes in Computer Science Volume 7795

Edition number

NEUVEDEN

Pages from

627

Pages to

629

Pages count

3

URL

Documents

BibTex


@inproceedings{BUT103454,
  author="Kamil {Dudka} and Petr {Müller} and Petr {Peringer} and Tomáš {Vojnar}",
  title="Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution)",
  annote="Predator is a tool for automated formal verification of sequential C programs
operating with pointers and linked lists. The core algorithms of Predator were
originally inspired by works on separation logic with higher-order list
predicates, but they are now purely graph-based and significantly extended to
support various forms of low-level memory manipulation used in system-level code.
This paper briefly introduces Predator and describes its participation in the
Software Verification Competition SV-COMP'13 held at TACAS'13.",
  address="Springer Verlag",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  chapter="103454",
  edition="Lecture Notes in Computer Science Volume 7795",
  howpublished="print",
  institution="Springer Verlag",
  number="7795",
  year="2013",
  month="march",
  pages="627--629",
  publisher="Springer Verlag",
  type="conference paper"
}