Predator: A Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic

Predator: Nástroj pro ověřování manipulace s dynamickými datovými strukturami založený na separační logice

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

Dudka Kamil, Ing.
Peringer Petr, Dr. Ing. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)

gcc, plug-in, separační logika, verifikace programů, C

Predator je praktický nástroj pro ověřování manipulace s dynamickými datovými strukturami založený na separační logice. Tento nástroj může být zaveden přímo do gcc jako plug-in (http://gcc.gnu.org/wiki/GCC_Plugins). Tímto způsobem je možné jednoduše analyzovat zdrojové kódy v jazyce C při použití existujícího systému pro sestavení, bez předchozího ručního předzpracování kódu atd. Samotná analýza však ještě není zcela připravena pro složitější projekty. Nástroj je založený na code-listner (http://www.fit.vutbr.cz/research/groups/verifit/tools/code-listener) infrastruktuře (zahrnuta).

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

• http://www.gnu.org/licenses/gpl-3.0.txt

Bezpečné, spolehlivé a adaptivní počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-10-1, 2010, ukončen
Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit, MŠMT, COST, OC10009, 2010-2012, řeš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í
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, 2007-2013, řešení

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

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