PredatorHP Attacks Interval-Sized Regions
This is an incremental improvement to a software verification tool for analyzing programs with dynamic memory.
The paper presents improvements to the PredatorHP shape analyzer, focusing on its enhanced handling of interval-sized memory regions for arrays with non-fixed sizes, and characterizes its performance in SV-COMP 2019, highlighting strengths and weaknesses influenced by these changes.
This paper describes shortly the basic principles of the PredatorHP (Predator Hunting Party) shape analyzer and presents its recent improvements. One of the most visible changes is the way PredatorHP handles interval-sized memory regions, which is particularly useful for dealing with arrays whose size is not fixed in advance. Further, the paper characterizes PredatorHP's participation in SV-COMP 2019, pointing out its strengths and weakness and the way they were influenced by the latest changes in the tool.