文章基本信息

标题：Saturation-Based Model Checking of Higher-Order Recursion Schemes
本地全文：下载
作者：Christopher Broadbent ; Naoki Kobayashi
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2013
卷号：23
页码：129-148
DOI：10.4230/LIPIcs.CSL.2013.129
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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