随着软件的迅速发展和广泛应用,并行程序在天气预测、石油勘探等一些重要领域的应用也越来越普遍。目前,OpenMP已经成为使用最广泛的并行编程语言。由于线程间执行顺序的非确定性,OpenMP比传统的串行程序更容易出错,同时程序错误难以重现,给程序的调试测试带来了很大的困难。并且,目前相关的OpenMP程序验证技术和验证工具也都还不成熟,这些因素使得当前OpenMP程序的正确性很难得到保证,严重阻碍了OpenMP程序的发展。为了更好的保障OpenMP程序的正确性,本文在一个高效的Pthreads程序验证工具Yogar-CBMC的基础上,研究了如何将其使用的限界模型检验等高效验证技术应用到OpenMP程序的验证中。首先,通过研究OpenMP程序的特点以及Yogar-CBMC所使用的限界模型检验、抽象精化和图分析等技术,本文提出了将OpenMP程序转换为更加底层的Pthreads程序,再利用Yogar-CBMC进行验证的思路。然后,基于Pthreads程序对OpenMP编译制导指令的语义进行了转换,将OpenMP程序转换成等价的Pthreads程序。通过修改开源的OpenMP编译器OMPi以及重写对应的Pthreads运行库,实现了将OpenMP程序自动转换为精简的Pthreads程序,然后利用Yogar-CBMC对转换后的Pthreads程序直接进行验证,扩展了Yogar-CBMC对OpenMP程序的支持。将Yogar-CBMC中的限界模型检验、抽象精化和图分析等高效验证技术应用到了OpenMP程序验证中,实现了OpenMP程序的高效验证。