随着软件的广泛应用,其规模越大越大,复杂度越来越高,软件的安全问题也越发突出。如何保证软件系统的正确性、可靠性和安全性,是计算机软件领域面临的重要挑战。作为一种自动化验证技术,模型检测可以有效地提升程序的安全性和可靠性。然而模型检测算法复杂度高,实现难度大,这也就成为对程序源码进行模型检测的主要瓶颈。通常,大多数模型检测工具都仅支持一种编程语言。LLVM是一个编译器框架,LLVM前端支持的任意编程语言都可以转为其中间表示LLVM IR。此外,LLVM IR还可以高效地使用LLVM的优化策略及分析方法,为程序分析及验证提供便利。本文研究LLVM IR程序的抽象验证理论与方法,从而可以支持多种程序设计语言的抽象验证。本文的主要工作内容和创新点如下:1.研究LLVM框架和LLVM IR的语法结构和基本语义,对LLVM IR程序进行词法分析和语法分析,提出了LLVM IR程序的CFA生成算法。2.根据LLVM IR程序的CFA,提出了基于CEGAR的LLVM IR程序验证方法,并根据该方法设计了相关验证工具的基本框架,具体给出了验证工具中各模块的设计与实现方案。并使用C++编程实现了该验证工具,可以实现对不同编程语言的程序进行验证。3.基于C程序和MSVL程序生成了大量的LLVM IR程序测试用例,用于测试基于CEGAR算法的LLVM IR程序验证工具,测试结果验证了该工具的正确性和可用性。