CPAlien: Configurable Program Analysis over Symbolic Memory Graphs
MÜLLER, P. VOJNAR, T.
CPAlien is a tool for verifying programs written in C language, manipulating with dynamic data structures. It is an instance of the Configurable Program Analysis based on the Symbolic Memory Graph formalism. The tool is implemented using the CPAChecker framework, developed and provided by University of Passau.
cpachecker, symbolic memory graphs, program verification, C language, static analysis