Detail produktu
Predator: A Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic
Vznik: 2010
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
vyžadována - zdarma
Autoři
Dudka Kamil, Ing. (UITS FIT VUT)
Peringer Petr, Dr. Ing. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Peringer Petr, Dr. Ing. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
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í
Licence
Projekty
Bezpečné, spolehlivé a adaptivní počítačové systémy (FIT-S-10-1)
Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit (OC10009)
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti (GAP103/10/0306)
Výzkum informačních technologií z hlediska bezpečnosti (MSM0021630528)
Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit (OC10009)
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti (GAP103/10/0306)
Výzkum informačních technologií z hlediska bezpečnosti (MSM0021630528)
Výzkumné skupiny
Pracoviště
Ústav inteligentních systémů FIT VUT v Brně (UITS FIT VUT)