中文摘要：

随着多核处理器的广泛使用以及人们对软件可靠性提出更高要求，多核并行程序验证的重要性日益凸显．本文提出了一个完整的基于多核的并行程序验证框架，该验证框架包括抽象机器定义、目标代码的形式规范、逻辑推理系统、可靠性定理及其证明．我们的目标程序使用自旋锁机制来实现线程间对共享内存的互斥访问．验证框架采用Hoare风格的推导方式，使用高阶逻辑来同时描述机器指令的操作语义和所需要的安全策略．在该框架下，程序员可以对多核并行程序的部分正确性进行验证．

英文摘要：

As the multi-core processor is widely used and advanced high-masted software is required,the verification of parallel programs for multi-core processor becomes more and more important. This paper presents a proof framework about the verification of parallel programs,including the definition of our abstract machine, the formal specification for object code, logic inference rules and the proof of soundness theory. The classic spin lock technology is introduced to implement the mutually exclusive access to shared memory. Our proof framework supports Hoare-logic style reasoning. In addition, we use high-order logic to describe both operational semantics and security policy. Programmers can verify the partial correctness of multi-core parallel programs in our framework.