Journal article

 
Dudka, K., Müller, P., Peringer, P., Vojnar, T.: Predator: A Verification Tool for Programs with Dynamic Linked Data Structures, In: Lecture Notes in Computer Science, Vol. 2012, No. 7214, DE, p. 544-547, ISSN 0302-9743
Publication language:english
Original title:Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution)
Title (cs):Predator: Nástroj pro verifikaci programů s dynamickými datovými strukturami
Pages:544-547
Place:DE
Year:2012
Journal:Lecture Notes in Computer Science, Vol. 2012, No. 7214, DE
ISSN:0302-9743
URL:http://www.springerlink.com/content/5x4748456031r18x/ [HTML]
Keywords
separation logic, shape analysis, dynamic linked data structures, pointers, linked lists, tool support, formal verification, Linux lists, Competition on Software Verification
Annotation
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.
BibTeX:
@ARTICLE{
   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 (Competition Contribution)},
   pages = {544--547},
   journal = {Lecture Notes in Computer Science},
   volume = {2012},
   number = {7214},
   year = {2012},
   ISSN = {0302-9743},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9845}
}