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

Název česky

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

Typ

software

Licence

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

Licenční poplatek

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

Autoři

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

Klíčová slova

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

Popis

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. 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 infrastruktuře (zahrnuta).

Umístění

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

Licenční podmínky

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

Projekty

Bezpečné, spolehlivé a adaptivní počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-10-1, zahájení: 2010-03-01, ukončení: 2010-12-31, ukončen
Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit, MŠMT, COST, OC10009, zahájení: 2010-01-01, ukončení: 2012-12-31, řešení
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti, GAČR, Standardní projekty, GAP103/10/0306, zahájení: 2010-01-01, ukončení: 2013-12-31, řešení
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení

Výzkumné skupiny

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

Pracoviště

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