Publication detail

Predator: A Verification Tool for Programs with Dynamic Linked Data Structures

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

Original Title

Predator: A Verification Tool for Programs with Dynamic Linked Data Structures

Type

journal article - other

Language

English

Original Abstract

Predator is a tool for automated formal verification of sequential C programs with dynamic linked data structures. It is in principle based on separation logic, but uses a graph-based heap representation. This paper first provides a brief overview of Predator and then discusses experience with its participation in the Software Verification Competition of TACAS'12.

Keywords

separation logic, shape analysis, dynamic linked data structures, pointers, linked lists, tool support, formal verification, Linux lists, Competition on Software Verification

Authors

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

RIV year

2012

Released

24. 3. 2012

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Year of study

2012

Number

7214

State

Federal Republic of Germany

Pages from

544

Pages to

547

Pages count

4

URL

http://www.springerlink.com/content/5x4748456031r18x/

BibTex

@article{BUT91458,
  author="Kamil {Dudka} and Petr {Müller} and Petr {Peringer} and Tomáš {Vojnar}",
  title="Predator: A Verification Tool for Programs with Dynamic Linked Data Structures",
  journal="Lecture Notes in Computer Science",
  year="2012",
  volume="2012",
  number="7214",
  pages="544--547",
  issn="0302-9743",
  url="http://www.springerlink.com/content/5x4748456031r18x/"
}