Faculty of Information Technology, BUT

Product Details

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

Created: 2010

Czech title
Predator: Nástroj pro ověřování manipulace s dynamickými datovými strukturami založený na separační logice
Type
software
License
required - free
Authors
Dudka Kamil, Ing. (DITS FIT BUT)
Peringer Petr, Dr. Ing. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Keywords
gcc, plug-in, separation logic, program verification, C
Description
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).
Location
Licence
Back to top