2014 | OriginalPaper | Buchkapitel
CPAlien: Shape Analyzer for CPAChecker
(Competition Contribution)
verfasst von : Petr Muller, Tomáš Vojnar
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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
extends 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.