This paper introduces PredatorHP (Predator Hunting Party). a program verifier built on top of the Predator shape analyser, and discusses its participation in the SV-COMP' 15 software verification competition. Predator is a sound shape analyser dealing with C programs with lists implemented via low-level pointer operations. PredatorHP uses Predator to prove programs safe while at the same time using several bounded versions of Predator for bug hunting.
展开▼
