C-SHORe：通过可塌陷下推系统饱和进行高阶验证
计算机科学中的逻辑
2018-09-18 v2
摘要
高阶递归方案（HORS）作为高阶函数式程序的一种有用抽象，已受到广泛关注，许多新的验证技术以 HORS 模型检验为核心。我们介绍了 C-SHORe 工具，它通过提供一种不同的自动机理论视角，为寻求真正可扩展的 HORS 模型检验器做出了贡献。C-SHORe 实现了第一个实用的模型检验算法，该算法作用于一种与 HORS 表达能力等价的、称为可塌陷下推系统（CPDS）的下推自动机推广形式。其核心是一个 CPDS 的后向饱和算法。此外，它能够利用从近似前向可达性分析中收集的信息来指导其后向搜索。此外，它使用了一种在模型检验前修剪 CPDS 的算法，以及一种在否定实例中提取反例的方法。我们提供了 C-SHORe 与最先进 HORS 验证工具的最新比较。该工具及附加材料可从 http://cshore.cs.rhul.ac.uk 获取。
引用
@article{arxiv.1703.04429,
title = {C-SHORe: Higher-Order Verification via Collapsible Pushdown System Saturation},
author = {Christopher Broadbent and Arnaud Carayol and Matthew Hague and Olivier Serre},
journal= {arXiv preprint arXiv:1703.04429},
year = {2018}
}