Result Details

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

DUDKA, K.; PERINGER, P.; VOJNAR, T. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. FIT-TR-2011-02, Brno: Faculty of Information Technology BUT, 2011. 23 p.
Type
report
Language
English
Authors
Dudka Kamil, Ing., DITS (FIT)
Peringer Petr, Dr. Ing., DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
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.

Keywords

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

URL
Published
2011
Pages
23
Publisher
Faculty of Information Technology BUT
Place
FIT-TR-2011-02, Brno
BibTeX 
@misc{BUT192766,
  author="Kamil {Dudka} and Petr {Peringer} and Tomáš {Vojnar}",
  title="Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic",
  year="2011",
  pages="23",
  publisher="Faculty of Information Technology BUT",
  address="FIT-TR-2011-02, Brno",
  url="http://www.fit.vutbr.cz/research/groups/verifit/tools/predator/FIT-TR-2011-02.pdf"
}
Projects
Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit, MŠMT, COST, OC10009, start: 2010-01-01, end: 2012-12-31, running
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness, GACR, Standardní projekty, GAP103/10/0306, start: 2010-01-01, end: 2013-12-31, running
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top