PV4 PredatorHP: Predator Hunting Partychecks memory-related errors and user-specified properties in C programs

Shape analyzer

Application domain/field

Expected input


Expected output

TRUE indicating that the specification is satisfied. FALSE indicating that the specification is violated. UNKNOWN if the tool could not determine whether the specification is satisfied or not.


PredatorHP is built on the Predator shape analyzer. PredatorHP looks for memory-related errors such as invalid pointer dereferences, double free operations and memory leaks. It also checks the validity of assertions in the code. PredatorHP runs multiple tools in parallel. The first tool is the Predator verifier, which can claim that a program is correct. The other tools are called hunters, which typically report errors. These hunters are used to decrease the chances of producing false alarms. TACAS'20: improved handling of interval-sized memory regions or new support of memory reallocation


License: GPL v3.0


Related papers

Last publication date

17 April 2020

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.