Saturation-Based Model Checking of Higher-Order Recursion Schemes

Authors Christopher Broadbent, Naoki Kobayashi



PDF
Thumbnail PDF

File

LIPIcs.CSL.2013.129.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)
https://doi.org/10.4230/LIPIcs.CSL.2013.129

Abstract

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.
Keywords
  • Model checking
  • higher-order recursion schemes
  • intersection types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail