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