Proof automation for functional correctness in separation logic
Proof automation for functional correctness in separation logic
复制标题
证明分离逻辑中功能正确性的自动化
DOI：
10.1093/logcom/exu032
复制
发表时间：
2016
影响因子：
0.7
通讯作者：
Maclean E
中科院分区：
文献类型：
--
作者：
Maclean E
我们描述了一种方法来自动证明指针程序，涉及迭代和递归的功能正确性。建立在分离逻辑，我们的方法已被实现为一个紧密集成的工具链，结合了一种新的组合证明规划和不变式生成。从形状分析，由Smallfoot静态分析仪进行，我们已经开发出一种证明策略，结合形状和功能方面的验证任务。通过关注迭代和递归代码，我们必须解决两个相关的不变量生成任务，即循环和框架不变量。我们处理这两个任务统一使用一种自动技术，称为长期合成，结合IsaPlanner/Isabelle定理证明。此外，在验证失败的情况下，我们试图通过自动生成缺失的先决条件来克服失败。我们详细介绍了我们的实验结果。我们的方法已经评估了一系列的例子，部分从功能扩展到Smallfoot语料库。
We describe an approach to automatically prove the functional correctness of pointer programs that involve iteration and recursion. Building upon separation logic, our approach has been implemented as a tightly integrated tool chain incorporating a novel combination of proof planning and invariant generation. Starting from shape analysis, performed by the Smallfoot static analyser, we have developed a proof strategy that combines shape and functional aspects of the verification task. By focusing on both iterative and recursive code, we have had to address two related invariant generation tasks, i.e. loop and frame invariants. We deal with both tasks uniformly using an automatic technique called term synthesis, in combination with the IsaPlanner/Isabelle theorem prover. In addition, where verification fails, we attempt to overcome failure by automatically generating missing preconditions. We present in detail our experimental results. Our approach has been evaluated on a range of examples, drawn in part from a functional extension to the Smallfoot corpus.
登录
查看更多内容
使用显式计划来指导归纳证明
DOI：
--
发表时间：
1988
期刊：
CADE
影响因子：
--
作者：
A. Bundy
通讯作者：
A. Bundy
DOI：
10.1007/978-3-540-45085-6_22
发表时间：
2003-07
期刊：
--
影响因子：
--
作者：
L. Dixon;Jacques D. Fleuriot
通讯作者：
L. Dixon;Jacques D. Fleuriot
一阶线性逻辑和其他无割序贯演算中的证明搜索
DOI：
10.1109/lics.1994.316061
发表时间：
1994
期刊：
Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
P. Lincoln;N. Shankar
通讯作者：
N. Shankar
VLSI规范、验证和综合
DOI：
10.1007/978-1-4613-2007-4
发表时间：
2013
期刊：
Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
G. Birtwistle;P. Subrahmanyam
通讯作者：
P. Subrahmanyam
链接数据结构中的突变
DOI：
10.1007/978-3-642-24559-6_20
发表时间：
2011
期刊：
Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
E. Maclean;Andrew Ireland
通讯作者：
Andrew Ireland