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

项目名称： 基于定理证明的多核并行程序验证

项目编号： No.61202038

项目类型： 青年科学基金项目

立项/批准年度： 2013

项目学科： 计算机科学学科

项目作者： 张南

作者单位： 西安电子科技大学

项目金额： 24万元

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

中文关键词： 定理证明；时序逻辑；多核；并行程序；形式化验证

英文摘要： To specify and verify multi-core parallel programs, a Cylinder Computation Model(CCM) is proposed based on Propositional Projection Temporal Logic(PPTL), the extended PPTL called CCM-PPTL is established including its syntax,semantics and logic laws. Further,the Normal Form (NF) and Normal Form Graph (NFG) are formalized, and satisfiability of CCM-PPTL formulas is investigated. Moreover, the set of axioms and inference rules of CCM-PPTL is defined; the axiomatic system of CCM-PPTL is formalized; the soundness and completeness of CCM-PPTL are also proved. In addition, to make the verification automatically, a prototype of theorem prover for CCM-PPTL based on PVS will be developed. Based on such a proof system and theorem prover, the methodology for specifying and verifying real multi-core parallel programs will be developed.

英文关键词： Theorem Proving；Temporal Logic；Multi-Core；Parallel Program；Formal Verification