CPAlien: Configurable Program Analysis over Symbolic Memory Graphs

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

software

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

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

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

cpachecker, symbolické paměťové grafy, verifikace programů, jazyk C, statická analýza programů

CPAlien je nástroj pro ověřování programů v jazyce C manipulujících s dynamickými datovými strukturami. Jedná se o instanci konfigurovatelné analýzy programů založené na formalismu symbolických paměťových grafů. Nástroj je implementován v rámci frameworku CPAChecker vyvíjeného na Passau Universitat. 

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

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

Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, 2011-2015, ukončen
Pokročilé bezpečné, spolehlivé a adaptivní IT, VUT, Vnitřní projekty VUT, FIT-S-11-1, 2011-2013, ukončen
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti, GAČR, Standardní projekty, GAP103/10/0306, 2010-2013, řešení
Verifikace a optimalizace počítačových systémů, VUT, Vnitřní projekty VUT, FIT-S-12-1, 2012-2014, ukončen

Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)

Ústav inteligentních systémů (UITS)