C-SHORe: A Collapsible Approach to Verifying Higher-Order Programs

Higher-order recursion schemes (HORS) have recently received much attention as a
useful abstraction of higher-order functional programs with a number of new verification
techniques employing HORS model-checking as their centrepiece. This paper
contributes to the ongoing quest for a truly scalable model-checker for HORS by
offering a different, automata theoretic perspective. We introduce the first
practical model-checking algorithm that acts on a generalisation of pushdown
automata equi-expressive with HORS called collapsible pushdown systems
(CPDS). At its core is a substantial modification of a recently studied
saturation algorithm for CPDS. In particular it is able to use information
gathered from an approximate forward reachability analysis to guide its backward
search. Moreover, we introduce an algorithm that prunes the CPDS prior to
model-checking and a method for extracting counter-examples in negative
instances. We compare our tool with the state-of-the-art verification tools for
HORS and obtain encouraging results.

In contrast to some of the main competition tackling the same problem, our algorithm is
fixed-parameter tractable, and we also offer significantly improved performance
over the only previously published tool of which we are aware that also enjoys
this property. The tool and additional material are available from
http://cshore.cs.rhul.ac.uk.