Publication result detail

CPAlien: Shape Analyzer for CPAChecker (Competition Contribution)

MÜLLER, P.; VOJNAR, T.

Original Title

CPAlien: Shape Analyzer for CPAChecker (Competition Contribution)

English Title

CPAlien: Shape Analyzer for CPAChecker (Competition Contribution)

Type

Paper in proceedings (conference paper)

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.

English 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

Key words in English

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

Authors

MÜLLER, P.; VOJNAR, T.

RIV year

2015

Released

05.04.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

Volume

8413

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 (Competition Contribution)",
  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"
}