Publication Details

CPAlien: Shape Analyzer for CPAChecker

MÜLLER, P.; VOJNAR, T. CPAlien: Shape Analyzer for CPAChecker. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2014. p. 395-397. ISBN: 978-3-642-54861-1.
Czech title
CPAlien: Analyzátor tvaru pro framework CPAChecker
Type
conference paper
Language
English
Authors
Müller Petr, Ing.
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
URL
Keywords

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

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.

Published
2014
Pages
395–397
Proceedings
Tools and Algorithms for the Construction and Analysis of Systems
Series
Lecture Notes in Computer Science
Volume
8413
ISBN
978-3-642-54861-1
Publisher
Springer Verlag
Place
Heidelberg
DOI
10.1007/978-3-642-54862-8_28
EID Scopus
2-s2.0-84900537327
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"
}
Back to top