基于分离逻辑的并行程序性质验证方法

摘要：

随着多核多线程并行执行方式的普及,并行程序形式化验证的需求日显突出.并行程序验证中执行流程的不确定性使验证的内容与目标的关系难以确定,且从并行程序直接进行性质验证会导致验证规模大.为此,提出一种基于分离逻辑的新的验证方法.该方法根据分离逻辑的程序语义描述兼有解释语义和公理语义的特点,从验证的性质出发,把要验证的性质式转换成并行语句序列的逻辑组合式,并进行整理和化简;然后,利用分离逻辑公理系统对语句序列进行验证,用验证了的断言集来求出性质的真值.实例进一步说明,此方法更有效,同时也简化了验证的规模.

关键词：霍尔逻辑、分离逻辑、并行程序、逻辑组合式、性质验证

所属期刊栏目：40

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金项目61070192,91018008,61170240;北京自然科学基金4122041;国家高技术研究发展计划2007AA01Z414;中国人民大学科学研究基金中央高校基本科研业务费专项资金项目成果+12XNLF06;贵州自然科学基金项目J[2011]2328

在线出版日期：2013-11-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：148-154