Detail publikace

CPAlien: Shape Analyzer for CPAChecker (Competition Contribution)

MÜLLER, P. VOJNAR, T.

Originální název

CPAlien: Shape Analyzer for CPAChecker (Competition Contribution)

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt


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.

Klíčová slova

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

Autoři

MÜLLER, P.; VOJNAR, T.

Rok RIV

2014

Vydáno

5. 4. 2014

Nakladatel

Springer Verlag

Místo

Heidelberg

ISBN

978-3-642-54861-1

Kniha

Tools and Algorithms for the Construction and Analysis of Systems

Edice

Lecture Notes in Computer Science

Strany od

395

Strany do

397

Strany počet

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