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

关键词：程序验证 多核处理器 自旋锁 汇编级代码 部分正确性 

单位：清华大学计算机科学与技术系; 北京100084; 清华大学软件学院; 北京100084