  This chapter, which is an extended and revised version of the conference
paper 'Predator: Byte-Precise Verification of Low-Level List Manipulation',
concentrates on a detailed description of the algorithms behind the Predator
shape analyser based on abstract interpretation and symbolic memory graphs.
Predator is particularly suited for formal analysis and verification of
sequential non-recursive C code that uses low-level pointer operations to
manipulate various kinds of linked lists of unbounded size as well as various
other kinds of pointer structures of bounded size. The tool supports
practically relevant forms of pointer arithmetic, block operations, address
alignment, or memory reinterpretation. We present the overall architecture of
the tool, along with selected implementation details of the tool as well as its
extension into so-called Predator Hunting Party, which utilises multiple
concurrently-running Predator analysers with various restrictions on their
behaviour. Results of experiments with Predator within the SV-COMP competition
as well as on our own benchmarks are provided.
