Conference paper

MÜLLER Petr and VOJNAR Tomáš. CPAlien: Shape Analyzer for CPAChecker. In: Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg: Springer Verlag, 2014, pp. 395-397. ISBN 978-3-642-54861-1. Available from:
Publication language:english
Original title:CPAlien: Shape Analyzer for CPAChecker (Competition Contribution)
Title (cs):CPAlien: Analyzátor tvaru pro framework CPAChecker
Proceedings:Tools and Algorithms for the Construction and Analysis of Systems
Conference:European Joint Conferences on Theory and Practice of Software -- ETAPS'14 (TACAS'14)
Series:LNCS 8413
Place:Heidelberg, DE
Publisher:Springer Verlag
shape analysis
configurable program analysis
static analysis
symbolic memory graphs
memory safety
software verification
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.
   author = {Petr M{\"{u}}ller and Tom{\'{a}}{\v{s}} Vojnar},
   title = {CPAlien: Shape Analyzer for CPAChecker
	(Competition Contribution)},
   pages = {395--397},
   booktitle = {Tools and Algorithms for the Construction and Analysis of
   series = {LNCS 8413},
   year = 2014,
   location = {Heidelberg, DE},
   publisher = {Springer Verlag},
   ISBN = {978-3-642-54861-1},
   doi = {10.1007/978-3-642-54862-8_28},
   language = {english},
   url = {}

Your IPv4 address:
Switch to https