Automating relatively complete verification of higher-order functional programs
Automating relatively complete verification of higher-order functional programs
复制标题
DOI：
10.1145/2429069.2429081
复制
发表时间：
2013-01
期刊：
影响因子：
--
通讯作者：
Hiroshi Unno;Tachio Terauchi;N. Kobayashi
中科院分区：
文献类型：
--
作者：
Hiroshi Unno;Tachio Terauchi;N. Kobayashi
我们提出了一种相对完整地验证安全性的自动化方法（即，可达性）属性的高阶函数程序。我们的贡献是双重的。首先，我们扩展了细化类型系统框架（不完全）自动化高阶验证最近的工作中使用的经典工作相对完整的“霍尔逻辑”程序逻辑高阶程序语言。然后，通过采用最近提出的技术解决约束的量化一阶逻辑公式，我们开发了一个自动类型推理方法的类型系统，从而实现了自动化的相对完整的验证高阶程序。
We present an automated approach to relatively completely verifying safety (i.e., reachability) property of higher-order functional programs. Our contribution is two-fold. First, we extend the refinement type system framework employed in the recent work on (incomplete) automated higher-order verification by drawing on the classical work on relatively complete "Hoare logic like" program logic for higher-order procedural languages. Then, by adopting the recently proposed techniques for solving constraints over quantified first-order logic formulas, we develop an automated type inference method for the type system, thereby realizing an automated relatively complete verification of higher-order programs.