Publication detail

CPAlien: Shape Analyzer for CPAChecker

MÜLLER, P. VOJNAR, T.

Original Title

CPAlien: Shape Analyzer for CPAChecker

English Title

CPAlien: Shape Analyzer for CPAChecker

Type

conference paper

Language

en

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

RIV year

2014

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

Edition number

NEUVEDEN

Pages from

395

Pages to

397

Pages count

3

URL

Documents

BibTex


@inproceedings{BUT111527,
  author="Petr {Müller} and Tomáš {Vojnar}",
  title="CPAlien: Shape Analyzer for CPAChecker",
  annote="
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.",
  address="Springer Verlag",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  chapter="111527",
  doi="10.1007/978-3-642-54862-8_28",
  edition="Lecture Notes in Computer Science",
  howpublished="print",
  institution="Springer Verlag",
  year="2014",
  month="april",
  pages="395--397",
  publisher="Springer Verlag",
  type="conference paper"
}