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

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

Software

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).

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).

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

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

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

only the provider uses the result

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

https://www.fit.vut.cz/research/product/149/