Discussing "Horn Clause Solvers for Program Verification"

(Link)

Authors: Nikolaj Bjørner (Microsoft Research Redmond), Arie Gurfinkel (Software Engineering Institute), Ken McMillan (Microsoft Research Redmond) & Andrey Rybalchenko (Microsoft Research Cambridge)

Reference: Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A. (2015). Horn Clause Solvers for Program Verification. In: Beklemishev, L., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds) Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. Lecture Notes in Computer Science, vol 9300. Springer, Cham. https://doi.org/10.1007/978-3-319-23534-9_2

Why this paper? Cited by Multiple Query Satisfiability of Constrained Horn Clauses and Parameterized Recursive Refinement Types for Automated Program Verification

This paper is a small jump away from my usual research area, based as it is on automatic program verification rather than interactive theorem proving, let alone some of my more pure interests in logic and mathematics. However it does bump up against one of my interests (Craig interpolation) and fortunately is a highly readable and not too technical survey article summarising a field of work.

Horn clauses come in various forms in this paper, but in general are a sharp constraint on the way in which logic formulae can be written down: instead of the freedom to use logical connectives wherever one desires, one must write one’s formula in a precisely specified structure. For example, all universal quantifiers might be required to be on the outside level rather than nested inside the formulae, there is a limit of one implication in the whole formulae between a ‘body’ and ‘head’ which themselves have strict rules regarding their construction, and so on. Formulae of first-order logic can be tortured until they fit the pattern required by a set of Horn clauses, albeit at some cost of time and space. Furthermore, in this paper the underlying logic is extended with an additional assertion language, usually something like a limited notion of arithmetic, which may be useful for expressing properties of programs.

The point of forcing us to write our logical statements in a highly constrained fashion is to find a compromise point between expressivity – we can talk in meaningful ways about the properties of interesting programs – and efficiency for automatic verification of these properties. After introducing the basic notions, this paper is roughly split between these two concerns. One half gives examples of various notions for turning both programs and interesting properties of these programs into Horn clauses, for example an approach based on weakest preconditions applied to the verification language Boogie. The other half looks at ways that Horn clauses can be transformed to support more successful automation. It is this half where Craig interpolation, a famous property from logical theory, intersects with the practical concerns of this paper, as a certain useful Horn clause transformation called ‘unfold’ can only be guaranteed to be sound if the underlying assertion logic enjoys the property.