CPAlien: Configurable Program Analysis over Symbolic Memory Graphs

Czech title

CPAlien: Konfigurovatelná analýza programů nad symbolickými paměťovými grafy

Type

software

License

required - free

Authors

Müller Petr, Ing. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)

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

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

Licence

http://www.apache.org/licenses/LICENSE-2.0.html

Projects

Advanced secured, reliable and adaptive IT (FIT-S-11-1)
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness (GAP103/10/0306)
The IT4Innovations Centre of Excellence (ED1.1.00/02.0070)
Verification and Optimization of Computer Systems (FIT-S-12-1)

Research groups

Automated Analysis and Verification Research Group - VeriFIT (VZ VERIFIT)

Departments

Department of Intelligent Systems FIT BUT (DITS FIT BUT)