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

Possibilities of use

K využití výsledku jiným subjektem je vždy nutné nabytí licence

Licence fee

Poskytovatel licence na výsledek nepožaduje licenční poplatek

www

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