Saturation-Based Model Checking of Higher-Order Recursion Schemes

Authors Christopher Broadbent, Naoki Kobayashi

Thumbnail PDF


  • Filesize: 0.65 MB
  • 20 pages

Document Identifiers

Author Details

Christopher Broadbent
Naoki Kobayashi

Cite AsGet BibTex

Christopher Broadbent and Naoki Kobayashi. Saturation-Based Model Checking of Higher-Order Recursion Schemes. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 129-148, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


Model checking of higher-order recursion schemes (HORS) has recently been studied extensively and applied to higher-order program verification. Despite recent efforts, obtaining a scalable model checker for HORS remains a big challenge. We propose a new model checking algorithm for HORS, which combines two previous, independent approaches to higher-order model checking. Like previous type-based algorithms for HORS, it directly analyzes HORS and outputs intersection types as a certificate, but like Broadbent et al.'s saturation algorithm for collapsible pushdown systems (CPDS), it propagates information backward, in the sense that it starts with target configurations and iteratively computes their pre-images. We have implemented the new algorithm and confirmed that the prototype often outperforms TRECS and CSHORe, the state-of-the-art model checkers for HORS.
  • Model checking
  • higher-order recursion schemes
  • intersection types


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads