随着多核处理器的广泛使用以及人们对软件可靠性提出更高要求,多核并行程序验证的重要性日益凸显。本文提出了一个完整的基于多核并行程序的验证框架MCAP,该验证框架包括了抽象机器定义、目标代码的形式规范、逻辑推理系统、可靠性定理及证明。最后,我们还在该框架的基础上提出了扩展思路和方法。MCAP框架采用直接在低级层次上进行验证的方式,避开了编译器正确性验证这一难题,目标程序使用自旋锁机制来实现线程间对共享内存的互斥访问。我们采用Hoare风格的推导方式,使用高阶逻辑来同时描述机器指令的操作语义和所需要的安全策略。在该框架下,程序员可以对多核并行程序的部分正确性进行验证。本文的主要贡献在于:1.提出了一个基于多核并行程序的验证框架MCAP,丰富了带证明代码(PCC)框架的应用形式和内容,同时也为多核并行程序验证提供了一种新的思路。2. MCAP框架是可靠的,我们使用辅助定理证明器Coq证明了关于该框架的可靠性定理。因此一个程序一旦经过该框架的验证,那么它将无需进行运行时检查,并且不会陷入滞留状态。3.对如何扩展MCAP框架进行了有效的分析,从真实汇编级验证,函数模块化验证和提高程序规范表达能力三个方面提出了扩展方法。