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)
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
Výzkumné skupiny
Pracoviště
Nahoru