Faculty of Information Technology, BUT

Product Details

CPAlien: Configurable Program Analysis over Symbolic Memory Graphs

Created: 2013

Czech title
CPAlien: Konfigurovatelná analýza programů nad symbolickými paměťovými grafy
Type
software
License
required - free
Authors
Keywords
cpachecker, symbolic memory graphs, program verification, C language, static analysis
Description
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.
Location
Licence
Back to top