Product Details
CPAlien: Configurable Program Analysis over Symbolic Memory Graphs
Created: 2013
Czech title
CPAlien: Konfigurovatelná analýza programů nad symbolickými paměťovými grafy
Type
software
License
In order to use the result by another entity, it is always necessary to acquire a license
License Fee
The licensor does not require a license fee for the result
Authors
Müller Petr, Ing.
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
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
License Conditions
Projects
Advanced secured, reliable and adaptive IT, BUT, Vnitřní projekty VUT, FIT-S-11-1, 2011-2013, completed
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness, GACR, Standardní projekty, GAP103/10/0306, 2010-2013, running
The IT4Innovations Centre of Excellence, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, 2011-2015, completed
Verifikace a optimalizace počítačových systémů, BUT, Vnitřní projekty VUT, FIT-S-12-1, 2012-2014, completed
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness, GACR, Standardní projekty, GAP103/10/0306, 2010-2013, running
The IT4Innovations Centre of Excellence, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, 2011-2015, completed
Verifikace a optimalizace počítačových systémů, BUT, Vnitřní projekty VUT, FIT-S-12-1, 2012-2014, completed
Research groups
Departments