Publication Details

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

DUDKA Kamil, MÜLLER Petr, PERINGER Petr and VOJNAR Tomáš. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures. Lecture Notes in Computer Science, vol. 2012, no. 7214, pp. 544-547. ISSN 0302-9743.

Czech title

Predator: Nástroj pro verifikaci programů s dynamickými datovými strukturami

Type

journal article

Language

english

Authors

Dudka Kamil, Ing. (DITS FIT BUT)
Müller Petr, Ing. (DITS FIT BUT)
Peringer Petr, Dr. Ing. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)

URL

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

Keywords

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

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.

Published

2012

Pages

544-547

Journal

Lecture Notes in Computer Science, vol. 2012, no. 7214, ISSN 0302-9743

Publisher

Springer Verlag

BibTeX

@ARTICLE{FITPUB9845,
   author = "Kamil Dudka and Petr M{\"{u}}ller and Petr Peringer and Tom\'{a}\v{s} Vojnar",
   title = "Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution)",
   pages = "544--547",
   journal = "Lecture Notes in Computer Science",
   volume = 2012,
   number = 7214,
   year = 2012,
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/9845"
}