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

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

software

In order to use the result by another entity, it is always necessary to acquire a license

The licensor does not require a license fee for the result

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

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

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 (http://gcc.gnu.org/wiki/GCC_Plugins). 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 (http://www.fit.vutbr.cz/research/groups/verifit/tools/code-listener) infrastructure (included).

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

• http://www.gnu.org/licenses/gpl-3.0.txt

Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit, MŠMT, COST, OC10009, 2010-2012, running
Secured, reliable and adaptive computer systems, BUT, Vnitřní projekty VUT, FIT-S-10-1, 2010, completed
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, 2007-2013, running
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness, GACR, Standardní projekty, GAP103/10/0306, 2010-2013, running

Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Department of Intelligent Systems (DITS)