Symbolic Execution Proofs for Higher Order Store Programs
Symbolic Execution Proofs for Higher Order Store Programs
复制标题
高阶存储程序的符号执行证明
DOI：
10.1007/s10817-014-9319-8
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Reus B
中科院分区：
文献类型：
--
作者：
Reus B
高阶存储程序是在运行时存储、操作和调用代码的程序。高阶存储程序的重要示例包括动态加载和卸载内核模块的操作系统内核。然而，传统的霍尔逻辑无法提供表示运行时代码更改的方法，因此不适用于此类程序。然而，最近，使用嵌套霍尔三元组的新逻辑解决了这个缺点。在本文中，我们从上到下描述了一个用于高阶存储程序的完善的半自动验证系统。我们给出一种具有高阶存储功能的编程语言，定义一种具有嵌套三元组的断言语言来指定此类程序，并提供推理规则来证明程序的正确性。然后，我们完整地展示了自动构建正确性证明的算法。与早期的工作相比，该语言还包括普通（固定）过程和可变局部变量，从而可以轻松对执行动态加载和其他高阶存储操作的程序进行建模。我们给出程序的操作语义和断言的步进索引解释，并使用它们来显示我们的推理规则的合理性，其中包括允许更多模块化证明的深层框架规则。我们的自动推理算法包括基于分离逻辑的程序符号执行方案，以及用于解决各种蕴涵问题的自动证明器。后者以派生证明规则集的形式呈现，这些规则受到足够的约束，可以作为证明搜索算法来读取。
Higher order store programs are programs which store, manipulate and invoke code at runtime. Important examples of higher order store programs include operating system kernels which dynamically load and unload kernel modules. Yet conventional Hoare logics, which provide no means of representing changes to code at runtime, are not applicable to such programs. Recently, however, new logics using nested Hoare triples have addressed this shortcoming. In this paper we describe, from top to bottom, a sound semi-automated verification system for higher order store programs. We give a programming language with higher order store features, define an assertion language with nested triples for specifying such programs, and provide reasoning rules for proving programs correct. We then present in full our algorithms for automatically constructing correctness proofs. In contrast to earlier work, the language also includes ordinary (fixed) procedures and mutable local variables, making it easy to model programs which perform dynamic loading and other higher order store operations. We give an operational semantics for programs and a step-indexed interpretation of assertions, and use these to show soundness of our reasoning rules, which include a deep frame rule which allows more modular proofs. Our automated reasoning algorithms include a scheme for separation logic based symbolic execution of programs, and automated provers for solving various kinds of entailment problems. The latter are presented in the form of sets of derived proof rules which are constrained enough to be read as a proof search algorithm.
登录
查看更多内容
DOI：
10.1007/s10009-015-0372-3
发表时间：
2015
期刊：
International journal on software tools for technology transfer : STTT
影响因子：
--
作者：
Blom S;Huisman M
通讯作者：
Huisman M
基于效果的程序转换的关系语义：高阶存储
DOI：
--
发表时间：
2009
期刊：
ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming
影响因子：
--
作者：
Nick Benton;A. Kennedy;Lennart Beringer;M. Hofmann
通讯作者：
M. Hofmann
DOI：
10.1145/1596550.1596565
发表时间：
2009
期刊：
ArXiv
影响因子：
--
作者：
A. Chlipala;G. Malecha;Greg Morrisett;Avraham Shinnar;Ryan Wisnesky
通讯作者：
Ryan Wisnesky
DOI：
10.1145/2318202.2318208
发表时间：
2012-06
期刊：
--
影响因子：
--
作者：
B. Horsfall;Nathaniel Charlton;Bernhard Reus
通讯作者：
B. Horsfall;Nathaniel Charlton;Bernhard Reus
Crowfoot：高阶存储程序的验证器
DOI：
10.1007/978-3-642-27940-9_10
发表时间：
2012
期刊：
2011 IEEE 27th International Conference on Data Engineering Workshops
影响因子：
--
作者：
Nathaniel Charlton;B. Horsfall;Bernhard Reus
通讯作者：
Bernhard Reus