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

Typ

software

Jazyk

anglicky

Autoři

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

Popis

Predator is a practical tool for checking manipulation of dynamic data structures using separation logic. It can be loaded directly into gcc as a plug-in. This way you can easily analyse C code sources, using the existing build system, without any manual preprocessing of them etc. The analysis itself is, however, not yet ready for complex projects yet. The plug-in is based on code-listner infrastructure (included).

Klíčová slova

gcc, plug-in, separation logic, program verification, C

Umístění

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

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

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)