Applied result detail

CPAlien: Configurable Program Analysis over Symbolic Memory Graphs

MÜLLER, P.; VOJNAR, T.

Original Title

CPAlien: Configurable Program Analysis over Symbolic Memory Graphs

English Title

CPAlien: Configurable Program Analysis over Symbolic Memory Graphs

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.

Abstract in English

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

Key words in English

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

Location

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

Licence fee

In order to use the result by another entity, it is always necessary to acquire a license

www

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