Conference paper

DUDKA Kamil, MÜLLER Petr, PERINGER Petr and VOJNAR Tomáš. Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution). In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer Verlag, 2013, pp. 627-629. ISBN 978-3-642-36742-7. ISSN 0302-9743.
Publication language:english
Original title:Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution)
Title (cs):Predator: Nástroj pro verifikaci nízkoúrovňové manipulace seznamů (soutěžní příspěvek)
Pages:627-629
Proceedings:Tools and Algorithms for the Construction and Analysis of Systems
Conference:European Joint Conferences on Theory and Practice of Software -- ETAPS'13 (TACAS'13)
Series:Lecture Notes in Computer Science Volume 7795
Place:Berlin, DE
Year:2013
ISBN:978-3-642-36742-7
Journal:Lecture Notes in Computer Science, Vol. 2013, No. 7795, DE
ISSN:0302-9743
Publisher:Springer Verlag
URL:http://link.springer.com/chapter/10.1007/978-3-642-36742-7_49 [HTML]
Keywords
dynamic linked data structures
separation logic
symbolic memory graphs
list manipulation
low-level memory manipulation
memory safety
shape analysis
Annotation
Predator is a tool for automated formal verification of sequential C programs operating with pointers and linked lists. The core algorithms of Predator were originally inspired by works on separation logic with higher-order list predicates, but they are now purely graph-based and significantly extended to support various forms of low-level memory manipulation used in system-level code. This paper briefly introduces Predator and describes its participation in the Software Verification Competition SV-COMP'13 held at TACAS'13.
BibTeX:
@INPROCEEDINGS{
   author = {Kamil Dudka and Petr M{\"{u}}ller and Petr Peringer and
	Tom{\'{a}}{\v{s}} Vojnar},
   title = {Predator: A Tool for Verification of Low-Level List
	Manipulation (Competition Contribution)},
   pages = {627--629},
   booktitle = {Tools and Algorithms for the Construction and Analysis of
	Systems},
   series = {Lecture Notes in Computer Science Volume 7795},
   journal = {Lecture Notes in Computer Science},
   volume = {2013},
   number = {7795},
   year = {2013},
   location = {Berlin, DE},
   publisher = {Springer Verlag},
   ISBN = {978-3-642-36742-7},
   ISSN = {0302-9743},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=10253}
}

Your IPv4 address: 54.224.21.195
Switch to IPv6 connection

DNSSEC [dnssec]