C-SHORe: A collapsible approach to verifying higher-order programs
Christopher H. Broadbent, Matthew Hague, Olivier Serre, Arnaud Carayol · 2013
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 employ-ing HORS model-checking as their centrepiece. This paper con-tributes 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 algo-rithm for CPDS. In particular it is able to use information gath-ered 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 encour-aging results. In contrast to some of the main competition tack-ling 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