Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification

Bishoksan Kafle, John P. Gallagher

We present an approach to constrained Horn clause (CHC) verification combining three techniques: abstract interpretation over a domain of convex polyhedra, specialisation of the co…