  We present an approach to constrained Horn clause (CHC) verification
combining three techniques: abstract interpretation over a domain of convex
polyhedra, specialisation of the constraints in CHCs using abstract
interpretation of query-answer transformed clauses, and refinement by splitting
predicates. The purpose of the work is to investigate how analysis and
transformation tools developed for constraint logic programs (CLP) can be
applied to the Horn clause verification problem. Abstract interpretation over
convex polyhedra is capable of deriving sophisticated invariants and when used
in conjunction with specialisation for propagating constraints it can
frequently solve challenging verification problems. This is a contribution in
itself, but refinement is needed when it fails, and the question of how to
refine convex polyhedral analyses has not been studied much. We present a
refinement technique based on interpolants derived from a counterexample trace;
these are used to drive a property-based specialisation that splits predicates,
leading in turn to more precise convex polyhedral analyses. The process of
specialisation, analysis and splitting can be repeated, in a manner similar to
the CEGAR and iterative specialisation approaches.
