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
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"
}
Back to top