C-SHORe: A Collapsible Approach to Verifying Higher-Order Programs. / Broadbent, Chris; Carayol, Arnaud; Hague, Matthew; Serre, Olivier.

ICFP: International Conference on Functional Programming. 2013. p. 13-24.

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



  • icfp13

    Accepted author manuscript, 205 KB, PDF document


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 Sep 2013
EventInternational Conference on Functional Programming - Boston, United Kingdom
Duration: 25 Sep 201327 Sep 2013


ConferenceInternational Conference on Functional Programming
CountryUnited Kingdom

Research outputs

This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 25572957