Product detail

CPAlien: Configurable Program Analysis over Symbolic Memory Graphs

MÜLLER, P. VOJNAR, T.

Product type

software

Abstract

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.

Keywords

cpachecker, symbolic memory graphs, program verification, C language, static analysis

Create date

18.12.2013

Location

http://www.fit.vutbr.cz/research/groups/verifit/tools/cpalien

www