Crowfoot: A Verifier for Higher-Order Store Programs
Crowfoot: A Verifier for Higher-Order Store Programs
复制标题
Crowfoot：高阶存储程序的验证器
DOI：
10.1007/978-3-642-27940-9_10
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Bernhard Reus
中科院分区：
文献类型：
--
作者：
Nathaniel Charlton;B. Horsfall;Bernhard Reus
我们提出了Crowfoot，一个自动验证工具的命令式程序，在运行时动态地操纵程序，这些程序使用的堆，不仅可以存储数据，但也代码（命令或程序）。这样的堆通常被称为高阶存储，并且允许例如动态地创建新的递归。可以使用高阶存储来对诸如代码的运行时加载和卸载、代码的运行时更新和运行时代码生成之类的现象进行建模。Crowfoot的断言语言，基于分离逻辑，具有嵌套的Hoare三元组，描述了存储在堆上的过程的行为。该工具解决了诸如深度框架规则和通过存储的递归等复杂问题，并且是基于具有嵌套三元组的Hoare逻辑的数学基础的最新发展的第一个验证工具。
We present Crowfoot, an automatic verification tool for imperative programs that manipulate procedures dynamically at runtime; these programs use a heap that can store not only data but also code (commands or procedures). Such heaps are often called higher-order store , and allow for instance the creation of new recursions on the fly. One can use higher-order store to model phenomena such as runtime loading and unloading of code, runtime update of code and runtime code generation. Crowfoot's assertion language, based on separation logic, features nested Hoare triples which describe the behaviour of procedures stored on the heap. The tool addresses complex issues like deep frame rules and recursion through the store, and is the first verification tool based on recent developments in the mathematical foundations of Hoare logics with nested triples.
关于运行时代码更新的形式化推理
DOI：
10.1109/icdew.2011.5767624
发表时间：
2011
期刊：
--
影响因子：
--
作者：
Charlton N
通讯作者：
Charlton N