Detail publikace

CPAlien: Shape Analyzer for CPAChecker

MÜLLER, P. VOJNAR, T.

Originální název

CPAlien: Shape Analyzer for CPAChecker

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