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)

Type

article in a collection out of WoS and Scopus

Language

English

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.

Keywords

dynamic linked data structures
separation logic
symbolic memory graphs
list manipulation
low-level memory manipulation
memory safety
shape analysis

Authors

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

RIV year

2013

Released

17. 3. 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

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Year of study

2013

Number

7795

State

Federal Republic of Germany

Pages from

627

Pages to

629

Pages count

3

URL

http://link.springer.com/chapter/10.1007/978-3-642-36742-7_49

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)",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  year="2013",
  series="Lecture Notes in Computer Science Volume 7795",
  journal="Lecture Notes in Computer Science",
  volume="2013",
  number="7795",
  pages="627--629",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-642-36742-7",
  issn="0302-9743",
  url="http://link.springer.com/chapter/10.1007/978-3-642-36742-7_49"
}