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

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

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

Licence

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

Projects

Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit (OC10009)
Secured, reliable and adaptive computer systems (FIT-S-10-1)
Security-Oriented Research in Information Technology (MSM0021630528)
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness (GAP103/10/0306)

Research groups

Automated Analysis and Verification Research Group - VeriFIT (VZ VERIFIT)
Formal verification and simulation for the design of secure systems (DC7-VZ)

Departments

Department of Intelligent Systems FIT BUT (DITS FIT BUT)