2026-07-24T11:52:18Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4194 2024-03-06T10:34:52Z ddc:004 open_access

Saturation-Based Model Checking of Higher-Order Recursion Schemes Broadbent, Christopher Kobayashi, Naoki Model checking higher-order recursion schemes intersection types 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christopher Broadbent and Naoki Kobayashi 2013 Is Part Of LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2013.129 urn:nbn:de:0030-drops-41941 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.129 eng https://creativecommons.org/licenses/by/3.0/legalcode