Publication detail

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

DUDKA, K. PERINGER, P. VOJNAR, T.

Original Title

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

Type

conference paper

Language

English

Original 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).

Keywords

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

Authors

DUDKA, K.; PERINGER, P.; VOJNAR, T.

RIV year

2014

Released

5. 4. 2014

Publisher

Springer Verlag

Location

Heidelberg

ISBN

978-3-642-54861-1

Book

Tools and Algorithms for the Construction and Analysis of Systems

Edition

Lecture Notes in Computer Science

Pages from

412

Pages to

414

Pages count

3

URL

http://link.springer.com/chapter/10.1007/978-3-642-54862-8_33

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"
}