Result Details

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

DUDKA, K.; PERINGER, P.; VOJNAR, T. 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. Heidelberg: Springer Verlag, 2014. p. 412-414. ISBN: 978-3-642-54861-1.
Type
conference paper
Language
English
Authors
Dudka Kamil, Ing.
Peringer Petr, Dr. Ing., DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Abstract

Predator is a shape analyzer that uses the abstract domain of symbolicmemory 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).

Keywords


dynamic linked data structures
separation logic
symbolic memory graphs
list manipulation
low-level memory manipulation
memory safety
shape analysis

URL
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)
ISBN
978-3-642-54861-1
Publisher
Springer Verlag
Place
Heidelberg
DOI
10.1007/978-3-642-54862-8_33
EID Scopus
2-s2.0-84900537246
BibTeX 
@inproceedings{BUT111526,
  author="Kamil {Dudka} and Petr {Peringer} and Tomáš {Vojnar}",
  title="Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution)",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  year="2014",
  series="Lecture Notes in Computer Science",
  volume="8413",
  pages="412--414",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-642-54862-8\{_}33",
  isbn="978-3-642-54861-1",
  url="http://link.springer.com/chapter/10.1007/978-3-642-54862-8_33"
}
Projects
Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures, GACR, Standardní projekty, GA14-11384S, start: 2014-01-01, end: 2016-12-31, completed
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, start: 2011-01-01, end: 2015-12-31, completed
Spolehlivost a bezpečnost v IT, BUT, Vnitřní projekty VUT, FIT-S-14-2486, start: 2014-01-01, end: 2016-12-31, completed
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top