Publication Details

CPAlien: Shape Analyzer for CPAChecker (Competition Contribution)

MÜLLER Petr and VOJNAR Tomáš. CPAlien: Shape Analyzer for CPAChecker. In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 8413. Heidelberg: Springer Verlag, 2014, pp. 395-397. ISBN 978-3-642-54861-1. Available from: http://link.springer.com/chapter/10.1007/978-3-642-54862-8_28
Czech title
CPAlien: Analyzátor tvaru pro framework CPAChecker
Type
conference paper
Language
english
Authors
Müller Petr, Ing. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
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
Conference
European Joint Conferences on Theory and Practice of Software -- ETAPS'14 (TACAS'14), Grenoble, FR
ISBN
978-3-642-54861-1
Publisher
Springer Verlag
Place
Heidelberg, DE
DOI
10.1007/978-3-642-54862-8_28
EID Scopus
2-s2.0-84900537327
BibTeX 
@INPROCEEDINGS{FITPUB10519,
   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 Systems",
   series = "Lecture Notes in Computer Science",
   volume = 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 = "https://www.fit.vut.cz/research/publication/10519"
}
Back to top