Verification of Higher-Order Programs

This project falls within the EPSRC Information and communication technologies (ICT) research area and it is related to Programming Languages and Compilers, Theoretical Computer Science as well as Verification and Correctness.

In recent years enormous progress in the development of SAT and SMT solvers has contributed significantly to the great scalability of verification tools for imperative programs using techniques such as Bounded Model Check and k-induction. However, techniques for the verification of (first-order) imperative programs do not seem to be appropriate for the verification of (higher-order) functional programs. Yet this programming paradigm is not only theoretically compelling but some of its features are now standard in historically imperative programming languages (Java, C++, Python, etc.), as well, and due to its restrictions on side effects it is appealing to developers of concurrent and distributed programs. Consequently, there is an increasing interest to find tools that verify functional, higher-order programs automatically.

Higher-order recursion schemes (HORS, or equivalently the _Y-calculus) are an attractive formalism to capture higher-order computation. In fact, order-n recursion schemes also represent the same class of trees as order-n collapsible pushdown automata, providing a neat automata theoretic characterisation. Thus, we are interested in model checking trees generated by HORS. Knapik et al. showed that the model checking problem with respect to monadic second order logic is decidable when a syntactic restriction is imposed on the HORS. Subsequently, Ong showed that this limitation is not necessary and that the model checking problem for order-n recursion schemes is n-EXPTIME complete. However, there has been considerable progress recently in the design of model checking algorithms, the best of which have polynomial fixed-parameter complexity in the size of the HORS (but obviously not in the order, and) and thus scale well when the number of rules is increased. Yet, a major obstacle towards further improving their effciency is that the known (higher-order) model checking approaches are mostly non-compositional, although functional programming facilitates writing highly compositional programs.

Further research challenges include finding algorithms for model checking directly higher-type trees, thus avoiding a translation to HORS (as by Kobayashi), which correspond to ground-type functional programs. However, an appropriate higher-type analogue to HORS still needs to be found since decidability is compromised by e.g. Bohm trees. More recently, have suggested that higher-order constrained horn clauses are a good basis for higherorder program verification paralleling the argument for the first-order setting. We have supported the claim by showing that complete proof systems exist using model theoretic insights and ideas from the theory of programming languages. However, there are many open problems, which are relevant for practice: Is it possible to restrict the proof system such that it can be used effciently in practice? Are there decidable fragments/special cases? Can the logic be extended without losing important properties such as completeness? Thus, the ultimate objective can be summarised as developing scalable, fully automatic and well-founded method for the verification of functional programs, based on higher-order model checking and constraint solving.