Detail produktu

CPAlien: Configurable Program Analysis over Symbolic Memory Graphs

MÜLLER, P. VOJNAR, T.

Typ produktu

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.

Klíčová slova

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

Datum vzniku

18. 12. 2013

Umístění

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

Možnosti využití

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

Licenční poplatek

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

www

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