CPAlien: Configurable Program Analysis over Symbolic Memory Graphs

Název česky

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

Typ

software

Licence

vyžadována - zdarma

Autoři

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

Klíčová slova

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

Popis

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.

Umístění

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

Licence

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

Projekty

Centrum excelence IT4Innovations (ED1.1.00/02.0070)
Pokročilé bezpečné, spolehlivé a adaptivní IT (FIT-S-11-1)
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti (GAP103/10/0306)
Verifikace a optimalizace počítačových systémů (FIT-S-12-1)

Výzkumné skupiny

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

Pracoviště

Ústav inteligentních systémů FIT VUT v Brně (UITS FIT VUT)