Detail aplikovaného výsledku

CPAlien: Configurable Program Analysis over Symbolic Memory Graphs

MÜLLER, P.; VOJNAR, T.

Originální název

CPAlien: Configurable Program Analysis over Symbolic Memory Graphs

Anglický název

CPAlien: Configurable Program Analysis over Symbolic Memory Graphs

Druh

Software

Abstrakt

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.

Abstrakt aglicky

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.

Klíčová slova

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

Klíčová slova anglicky

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

Umístění

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

Licenční poplatek

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

www

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