Higher-order constrained Horn clauses for higher-order program verification

Thesis

Higher-order constrained Horn clauses (HoCHC) are a fragment of higher-order logic modulo theories recently introduced by Cathcart Burn et al. (2018). This thesis explores the adequacy of HoCHC as a unifying framework for the algorithmic verification of higher-order programs, through links with existing approaches to program verification as well as a sound and refutationally complete solution method for HoCHC.

We establish a continuous interpretation for HoCHC in which the semantic domains are restricted to Scott-continuous functions. We show that the continuous HoCHC decision problem is equivalent to the original problem. This continuous interpretation serves as a foundation for a sound and refutation-complete resolution proof system - based on SLD-resolution - for solving unsatisfiable instances of the HoCHC problem over a semi-decidable background theory.

To address the relation between HoCHC and higher-order model checking, we introduce a coinductive version of HoCHC that is characterised by a greatest fixpoint construction. We define an encoding of higher-order recursion schemes into a HoCHC logic program, which can be used to reduce the open higher-order recursion scheme equivalence problem - and thus the lambdaY-calculus Böhm tree equivalence problem - to semi-decidability of coinductive HoCHC over Maher's complete and decidable background theory of trees (Maher, 1988; Djelloul et al., 2008).

Finally, we develop an axiomatic basis for relations as higher-order program invariants in the form of a Hoare logic. Our approach to Hoare logic for higher-order programs distinguishes itself from the literature through the combination of a higher-order assertion logic and a relatively complete proof system.

Authors: Jochems, J

• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: resolution; higher-order model checking; higher-order recursion schemes; Horn clauses; higher-order program verification; Hoare logic; program verification; coinduction; higher-order constrained Horn clauses; higher-order logic
• Subjects: Computer science (mathematics)