基于定理证明的多核并行程序验证

基金项目类型：

国家自然科学基金

基金项目编号：

61202038

来源网站：

国家自然科学基金委员会

来源网址：

http://www.nsfc.gov.cn/

负责人：

张南

完成单位：

西安电子科技大学

中文关键词：

定理证明; 时序逻辑; 多核; 并行程序; 形式化验证;

其他语种关键词：

Theorem Proving; Temporal Logic; Multi-Core; Parallel Program; Formal Verification

项目类型：

青年科学基金项目

语种：

中文

开始日期：

2013-01-01

结束日期：

2015-12-31

中文摘要：

扩展命题投影时序逻辑Propositional Projection Temporal Logic(PPTL)，提出适合描述多核并行程序的柱面计算模型Cylinder Computation Model(CCM)，建立扩展的命题投影时序逻辑CCM-PPTL系统。研究它的语法，语义和逻辑规则，研究它的范式，范式图及可判定性。定义CCM-PPTL的公理和推理规则，建立CCM-PPTL的公理系统；证明该公理系统的合理性和完备性。对PPTL定理证明器进行扩展，实现基于PVS的CCM-PPTL证明器原型。建立基于CCM-PPTL公理系统和证明器对多核并行程序进行验证的理论和方法。