HMC: Verifying Functional Programs Using Abstract Interpreters
HMC: Verifying Functional Programs Using Abstract Interpreters
复制标题
HMC：使用抽象解释器验证功能程序
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
A. Rybalchenko
中科院分区：
文献类型：
--
作者：
Ranjit Jhala;R. Majumdar;A. Rybalchenko
我们提出了 Hindley-Milner-Cousots (HMC)，这是一种算法，可将类型化高阶函数程序的安全属性验证简化为一阶命令式程序的过程间分析。 HMC 的工作原理如下。首先，它利用函数程序的类型结构生成一组逻辑细化约束，其满足意味着源程序的安全性。接下来，它将逻辑细化约束转换为简单的一阶命令式程序和一个保持当且仅当约束可满足的不变量。最后，它使用一阶命令式程序的不变量生成器来释放不变量。我们已经实现了 HMC 并使用两个命令式检查器（ARMC 和 INTERPROC）描述了初步实验结果，以验证 OCAML 程序。通过组合基于程序语法的基于类型的推理和基于抽象解释的基于状态的推理，HMC 能够对用现代编程语言编写的程序进行全自动验证。
We present Hindley-Milner-Cousots (HMC), an algorithm that reduces verification of safety properties of typed higher-order functional programs to interprocedural analysis for first-order imperative programs. HMC works as follows. First, it uses the type structure of the functional program to generate a set of logical refinement constraints whose satisfaction implies the safety of the source program. Next, it transforms the logical refinement constraints into a simple first-order imperative program and an invariant that holds iff the constraints are satisfiable. Finally, it uses an invariant generator for first-order imperative programs to discharge the invariant. We have implemented HMC and describe preliminary experimental results using two imperative checkers - ARMC and INTERPROC - to verify OCAML programs. By composing type-based reasoning grounded in program syntax and state-based reasoning grounded in abstract interpretation, HMC enables the fully automatic verification of programs written in modern programming languages.