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

Chris Broadbent, Arnaud Carayol, Matthew Hague, Olivier Serre

Research output: Chapter in Book/Report/Conference proceedingConference contribution

84 Downloads (Pure)


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
Original languageEnglish
Title of host publicationICFP: International Conference on Functional Programming
Number of pages12
Publication statusPublished - 25 Sept 2013
EventInternational Conference on Functional Programming - Boston, United Kingdom
Duration: 25 Sept 201327 Sept 2013


ConferenceInternational Conference on Functional Programming
Country/TerritoryUnited Kingdom

Cite this