基于分离逻辑的并行程序性质验证方法
外文标题：Verification Method for Concurrent Programs Properties Based on Separation Logic
文献类型：期刊
作者：万良[1]
机构：[1]中国人民大学信息学院
[2]中国人民大学数据工程与知识工程重点实验室
[3]贵州大学计算机科学与信息学院
年：2013
期刊名称：计算机科学
卷：40
期：10
页码范围：148-154
增刊：增刊
收录情况：中文核心期刊要目总览
所属部门：信息学院
语言：中文
ISSN：1002-137X
链接地址：http://d.g.wanfangdata.com.cn/Periodical_jsjkx201310031.aspx
DOI：10.3969/j.issn.1002-137X.2013.10.031
人气指数：11
浏览次数：11
基金：国家自然科学基金项目; 北京自然科学基金; 国家高技术研究发展计划; 中国人民大学科学研究基金(中央高校基本科研业务费专项资金)项目成果; 贵州自然科学基金项目
关键词：霍尔逻辑;分离逻辑;并行程序;逻辑组合式;性质验证
摘要：随着多核多线程并行执行方式的普及,并行程序形式化验证的需求日显突出.并行程序验证中执行流程的不确定性使验证的内容与目标的关系难以确定,且从并行程序直接进行性质验证会导致验证规模大.为此,提出一种基于分离逻辑的新的验证方法.该方法根据分离逻辑的程序语义描述兼有解释语义和公理语义的特点,从验证的性质出发,把要验证的性质式转换成并行语句序列的逻辑组合式,并进行整理和化简;然后,利用分离逻辑公理系统对语句序列进行验证,用验证了的断言集来求出性质的真值.实例进一步说明,此方法更有效,同时也简化了验证的规模.
作者其他论文
基于隔离逻辑的并行程序可靠性验证方法.万良.计算机工程.2014,86-91,96.
磁盘阵列环境下的取证目标系统重构.杨勇;石文昌;梁彬,等.计算机应用与软件.2014,64-67,74.
一种基于CIL静态分析的C#程序缺陷检测方法.边攀;梁彬;石文昌.计算机科学.2014,41(1),220-224.
一种在Android中植入动态污点分析模块的方法.梁彬;游伟;王鹏,等.2013.
基于特征扫描的Windows回收站删除记录取证方法..0.
