| 分离逻辑的技术基础与研究现状 |
| |
| 引用本文： | 王捍贫,张博闻.分离逻辑的技术基础与研究现状[J].广州大学学报(自然科学版),2019,18(2). |
| |
| 作者姓名： | 王捍贫 张博闻 |
| |
| 作者单位： | 广州大学计算机科学与网络工程学院,广东广州510006;北京大学信息科学技术学院软件研究所,北京100871;北京大学高可信软件技术教育部重点实验室,北京100871;北京大学信息科学技术学院软件研究所,北京100871;北京大学高可信软件技术教育部重点实验室,北京100871 |
| |
| 摘 要： | 随着计算机系统复杂性的日渐增加,可靠性正成为计算机软件理论中新的研究热点.运用数理逻辑中的推理方法,研究人员可以严格分析和验证计算机程序的正确性.分离逻辑作为一种分析共享可操作存储程序的新方法,近年来逐渐发展成为针对可扩展程序的主流验证技术之一.文章阐述分离逻辑的研究背景、理论基础以及验证原理,详细介绍其对存储空间抽象描述的思想,通过实例说明分离逻辑的推导策略.特别地,介绍了双向诱导推理对循环链表程序片段的验证过程,展现了在未知系统当前状态的情况下,分离逻辑验证未完成代码,甚至代码片段正确性的可行性.文章还综述了诸多基于分离逻辑的各种拓展,以增加对分离逻辑研究状况的了解.
|
| 关 键 词： | 分离逻辑 形式化方法 双向诱导推理 程序验证 |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
