Publication Details

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

DUDKA, K.; MÜLLER, P.; PERINGER, P.; VOJNAR, T. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7214, p. 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.
Müller Petr, Ing.
Peringer Petr, Dr. Ing. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
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
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/"
}
Back to top