Publication Details

Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution)

DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution). In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 8413. Heidelberg: Springer Verlag, 2014, pp. 412-414. ISBN 978-3-642-54861-1. Available from: http://link.springer.com/chapter/10.1007/978-3-642-54862-8_33
Czech title
Predator: analyzátor tvaru založený na symbolických grafech paměti (soutěžní příspěvek)
Type
conference paper
Language
english
Authors
Dudka Kamil, 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 shape analyzer that uses the abstract domain of symbolic memory graphs in order to support various forms of low-level memory manipulation commonly used in optimized C code. This paper briefly describes the verification approach taken by Predator and its strengths and weaknesses revealed during its participation in the Software Verification Competition (SV-COMP14).

Published
2014
Pages
412-414
Proceedings
Tools and Algorithms for the Construction and Analysis of Systems
Series
Lecture Notes in Computer Science
Volume
8413
Conference
European Joint Conferences on Theory and Practice of Software -- ETAPS'14 (TACAS'14), Grenoble, FR
ISBN
978-3-642-54861-1
Publisher
Springer Verlag
Place
Heidelberg, DE
DOI
10.1007/978-3-642-54862-8_33
EID Scopus
2-s2.0-84900537246
BibTeX 
@INPROCEEDINGS{FITPUB10518,
   author = "Kamil Dudka and Petr Peringer and Tom\'{a}\v{s} Vojnar",
   title = "Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution)",
   pages = "412--414",
   booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
   series = "Lecture Notes in Computer Science",
   volume = 8413,
   year = 2014,
   location = "Heidelberg, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-642-54861-1",
   doi = "10.1007/978-3-642-54862-8\_33",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10518"
}
Back to top