Higher-Order Constrained Horn Clauses and Automated Program Verification

Steven Ramsay

One of the most basic problems in automatic program verification is program safety, the problem of deciding whether or not a given program can ever reach a "bad state", such as an error condition. It is well known that program safety can be witnessed by finding a suitable invariant. For first-order programs, such invariants can be characterised, in first-order logic, as the models of certain systems of constrained Horn clauses. In 2012, Bjørner, McMillan and Rybalchenko initiated a research programme advocating first-order constrained Horn clauses as a logical basis for automatic program verification and the subject has attracted intensive study in the years since.

We introduce constrained Horn clauses in higher-order logic and study their satisfiability problem, motivated by the automatic verification of higher-order programs. Although satisfiable systems of higher-order clauses in the standard semantics do not generally have least models, we show that there is a non-standard semantics that does satisfy the least model property. Moreover the respective satisfiability problems in the standard and non-standard semantics are inter-reducible. We exploit the non-standard semantics in an automated solver based on refinement type inference.