Publication detail

CPAlien: Shape Analyzer for CPAChecker

MÜLLER, P. VOJNAR, T.

Original Title

CPAlien: Shape Analyzer for CPAChecker

Type

conference paper

Language

English

Original Abstract

CPALien is a configurable program analysis framework instance. It uses an extension of the symbolic memory graphs (SMGs) abstract domain for shape analysis of programs manipulating the heap. In particular, CPAlien ex- tends SMGs with a simple integer value analysis in order to handle programs with both pointers and integer data. The current version of CPAlien is an early prototype intended as a basis for a future research in the given area. The version submitted for SV-COMP'14 does not contain any shape abstraction, but it is still powerful enough to participate in several categories.

Keywords

shape analysis configurable program analysis static analysis symbolic memory graphs memory safety software verification

Authors

MÜLLER, 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

395

Pages to

397

Pages count

3

URL

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

BibTex

@inproceedings{BUT111527,
  author="Petr {Müller} and Tomáš {Vojnar}",
  title="CPAlien: Shape Analyzer for CPAChecker",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  year="2014",
  series="Lecture Notes in Computer Science",
  volume="8413",
  pages="395--397",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-642-54862-8\{_}28",
  isbn="978-3-642-54861-1",
  url="http://link.springer.com/chapter/10.1007/978-3-642-54862-8_28"
}