Higher-Order Constrained Horn Clauses for verification

Lead Research Organisation: University of Oxford
Department Name: Computer Science

Abstract

EPSRC Themes: Verification and Correctness; Programming Languages and Compilers
Higher-Order Verification is concerned with higher-order functions, which are essential to functional programming and cannot be handled by traditional model checkers for imperative, first-order programs. Besides its theoretical beauty, the functional paradigm also enjoys growing interest and use outside academia, with popular programming languages like Java 8 and C++11 adopting functional features. This makes it more important to study higher-order programs in more detail and in particular, the verification problem for such programs.
One approach to the verification problem of higher-order programs is via a translation to higher-order recursion schemes (HORS), which are equivalent to the (Lambda)Y-calculus, i.e. the simply typed (Lambda)-calculus with fixed point combinators. In 2006, Ong proved that model-checking trees generated by HORS is decidable with respect to monadic second-order properties Since then, a lot of theory has been established, using various concepts from theoretical computer science: In 2009, Kobayashi and Ong proved that model checking can be reduced to a type checking problem, making use of intersection types; in 2017, order-n recursion schemes were shown to generate the same class of trees as order-n collapsible push-down automata.
Like many verification problems, the worst-case time complexity of higher-order model checking is extremely poor - checking trees generated by order-n recursion schemes is n-EXPTIME-complete. However, fixed-parameter polynomial time algorithm have been developed, which scale to instances with thousands of rules in practice.
A very recent innovation in higher-order verification are higher-order constrained Horn clauses (HoCHC). Previously, Bjorner et al. had advocated the use of constrained Horn clauses for (first-order) model checking and they are now used a lot in the first-order case. HoCHCs are an extension of this to higher-order logic, which allows expressing Horn constraints over higher-order functions. They promise to provide a language-agnostic way of specifying functional invariants. Via a defunctionalization algorithm, HoCHCs can also be translated to FoCHCs to make use of the available efficient solvers for the latter. Recently, a sound and refutationally complete resolution proof system for HoCHCs has been found.
As HoCHCs are a very new approach, there are numerous avenues of exploration, such as illuminating its relationship with HoMC and refinement typability. Higher-order constraints may even prove useful in first-order verification, e.g. type constructors are modelled very naturally as a higher-order relation.
The work will take place in the Programming Languages and Verification Group at the Department of Computer Science at the University of Oxford where several other doctoral students have worked on HoCHC. There may also be a fruitful collaboration with Steven Ramsay, who was at Oxford until recently and is now a lecturer at the University of Bristol, and his research group.

Publications

10 25 50

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509711/1 01/10/2016 30/09/2021
2285273 Studentship EP/N509711/1 01/10/2019 31/03/2023 Fabian Zaiser Zaiser
EP/R513295/1 01/10/2018 30/09/2023
2285273 Studentship EP/R513295/1 01/10/2019 31/03/2023 Fabian Zaiser Zaiser