论文标题
验证ML程序的LIVESE属性
Verifying Liveness Properties of ML Programs
论文作者
论文摘要
高阶递归方案是布尔计划的高阶类似物；它们构成了功能程序的天然抽象类别。我们提出了一种新的，有效的算法，用于检查由高阶递归方案生成的树的CTL属性，这是Kobayashi基于Kobayashi的基于相交类型的模型检查技术的扩展。我们表明，该算法（THORS）的实现在许多小示例上都表现良好，我们演示了如何使用它来验证OCAML程序的可笑性属性。示例属性包括语句，例如“所有打开的插座最终都关闭了”和“锁定锁定直到文件关闭”。
Higher-order recursion schemes are a higher-order analogue of Boolean Programs; they form a natural class of abstractions for functional programs. We present a new, efficient algorithm for checking CTL properties of the trees generated by higher-order recursion schemes, which is an extension of Kobayashi's intersection type-based model checking technique. We show that an implementation of this algorithm, THORS, performs well on a number of small examples and we demonstrate how it can be used to verify liveness properties of OCaml programs. Example properties include statements such as "all opened sockets are eventually closed" and "the lock is held until the file is closed".
