Technical report

 
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, CZ, FIT VUT, 2011, p. 23
Publication language:english
Original title:Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic
Title (cs):Predator: Nástroj pro ověřování manipulace s dynamickými datovými strukturami založený na separační logice
Pages:23
Place:FIT-TR-2011-02, Brno, CZ
Year:2011
Publisher:Faculty of Information Technology BUT
URL:http://www.fit.vutbr.cz/research/groups/verifit/tools/predator/FIT-TR-2011-02.pdf [HTML]
Keywords
separation logic, shape analysis, dynamic linked data structures, pointers, linked lists, tool support, formal verification, Linux lists
Annotation
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.
BibTeX:
@TECHREPORT{
   author = {Kamil Dudka and Petr Peringer and Tomáš Vojnar},
   title = {Predator: A Practical Tool for Checking Manipulation of
	Dynamic Data Structures Using Separation Logic},
   pages = {23},
   year = {2011},
   location = {FIT-TR-2011-02, Brno, CZ},
   publisher = {Faculty of Information Technology BUT},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9723}
}