Predator: A Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic |
| Authors: | Dudka Kamil, Peringer Petr, Vojnar Tomáš |
|---|
| Type: | software |
| Created: | 2010 |
| Licence: | required - no fee | | 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: |
|---|
|
| Research groups: |
|---|
|
| Departments: |
|---|
|
| Licence terms: |
|---|
|
|
Faculty of Information Technology