Publication result detail

Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution)

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

Original Title

Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution)

English Title

Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution)

Type

Peer-reviewed article not indexed in WoS or Scopus

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.

English 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

Key words in English

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

2013

Released

24.03.2012

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Volume

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 (Competition Contribution)",
  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/"
}