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

Autoři:Dudka Kamil, Peringer Petr, Vojnar Tomáš
Typ:software
Vznik:2010
Licence:vyžadována - zdarma
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í:
Výzkumné skupiny:
Pracoviště:
Licenční podmínky:

Vaše IPv4 adresa: 34.238.189.171
Přepnout na https