Publication Details

Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic

DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. Lecture Notes in Computer Science, vol. 2011, no. 6806, pp. 372-378. ISSN 0302-9743.
Czech title
Predator: Nástroj pro ověřování manipulace s dynamickými datovými strukturami založený na separační logice
Type
journal article
Language
english
Authors
Dudka Kamil, 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

Abstract

Predator is a new open source tool for verification of sequential C programs with dynamic linked data structures. The tool is conceptually based on separation logic with inductive predicates despite it uses a graph description of heaps. Predator currently handles various forms of lists, including singly-linked as well as doubly-linked lists that may be circular, hierarchically nested and that may have various additional pointer links. Predator is implemented as a gcc plug-in and it is capable of handling lists in the form they appear in real system code, especially the Linux kernel, including a limited support of pointer arithmetic. Collaboration on further development of Predator is welcome.

Published
2011
Pages
372-378
Journal
Lecture Notes in Computer Science, vol. 2011, no. 6806, ISSN 0302-9743
Publisher
Springer Verlag
BibTeX
@ARTICLE{FITPUB9524,
   author = "Kamil Dudka and Petr Peringer and Tom\'{a}\v{s} Vojnar",
   title = "Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic",
   pages = "372--378",
   journal = "Lecture Notes in Computer Science",
   volume = 2011,
   number = 6806,
   year = 2011,
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/9524"
}
Back to top