Publication Details

Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution)

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. Lecture Notes in Computer Science Volume 7795, vol. 2013. Berlin: Springer Verlag, 2013, pp. 627-629. ISBN 978-3-642-36742-7. ISSN 0302-9743.
Czech title
Predator: Nástroj pro verifikaci nízkoúrovňové manipulace seznamů (soutěžní příspěvek)
Type
conference paper
Language
english
Authors
Dudka Kamil, Ing. (DITS FIT BUT)
Müller Petr, Ing. (DITS FIT BUT)
Peringer Petr, Dr. Ing. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords
dynamic linked data structures
separation logic
symbolic memory graphs
list manipulation
low-level memory manipulation
memory safety
shape analysis
Abstract

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.

Published
2013
Pages
627-629
Journal
Lecture Notes in Computer Science, vol. 2013, no. 7795, ISSN 0302-9743
Proceedings
Tools and Algorithms for the Construction and Analysis of Systems
Series
Lecture Notes in Computer Science Volume 7795
Conference
European Joint Conferences on Theory and Practice of Software -- ETAPS'13 (TACAS'13), Řím, IT
ISBN
978-3-642-36742-7
Publisher
Springer Verlag
Place
Berlin, DE
BibTeX 
@INPROCEEDINGS{FITPUB10253,
   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 = "https://www.fit.vut.cz/research/publication/10253"
}
Back to top