Journal article

 
Dudka, K., Peringer, P., Vojnar, T.: Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic, In: Lecture Notes in Computer Science, Vol. 2011, No. 6806, DE, p. 372-378, ISSN 0302-9743
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:372-378
Place:DE
Year:2011
Journal:Lecture Notes in Computer Science, Vol. 2011, No. 6806, DE
ISSN:0302-9743
URL:http://www.springerlink.com/content/0348r4140k031426/ [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:
@ARTICLE{
   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 = {372--378},
   journal = {Lecture Notes in Computer Science},
   volume = {2011},
   number = {6806},
   year = {2011},
   ISSN = {0302-9743},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9524}
}