# C-SHORe: Higher-Order Verification via Collapsible Pushdown System Saturation

## TL;DR

C-SHORe introduces a scalable, automata-theoretic model-checking approach for higher-order recursion schemes using collapsible pushdown systems, enhancing verification efficiency and providing counter-examples.

## Contribution

It presents the first practical model-checking algorithm for CPDS, integrating backward saturation, forward guidance, pruning, and counter-example extraction.

## Key findings

- Effective backward saturation algorithm for CPDS
- Guided model-checking using forward reachability information
- Competitive performance compared to state-of-the-art tools

## Abstract

Higher-order recursion schemes (HORS) have 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. We give an account of the C-SHORe tool, which contributed to the ongoing quest for a truly scalable model-checker for HORS by offering a different, automata theoretic perspective. C-SHORe implements 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 backwards saturation algorithm for CPDS. Additionally, it is able to use information gathered from an approximate forward reachability analysis to guide its backward search. Moreover, it uses an algorithm that prunes the CPDS prior to model-checking and a method for extracting counter-examples in negative instances. We provide an up-to-date comparison of C-SHORe with the state-of-the-art verification tools for HORS. The tool and additional material are available from http://cshore.cs.rhul.ac.uk.