随着计算机技术的快速发展,软件已经成为决定系统安全性的关键因素。程序代码作为软件的核心,细小的错误都可能导致严重的安全事故。对于程序中运行时错误的验证是确保软件安全至关重要的一环。工业界常用的仿真、模拟、测试等手段可以发现大部分运行时错误,但却无法保证软件中没有运行时错误。已有的形式化静态分析方法如模型检测需要穷举所有状态空间,存在状态空间爆炸问题;定理证明需要大量人工参与,难以自动化;抽象解释对程序语义进行抽象,是验证运行时错误最合适的分析方法之一。为了满足工业需求,静态分析常常要根据不同需求调整分析过程的精度和效率,可配置程序分析是一种通过配置参数调整分析过程精度和效率的静态分析框架,适合对抽象解释的分析过程进行建模。本文提出并扩展了一种支持抽象解释的静态分析形式化体系框架,即可配置程序分析。使用基于可配置程序分析的抽象解释分析方法,在抽象环境中模拟程序实际运行时所有可能达到的状态,对运行时错误进行了分析和验证。论文主要工作如下。(1)对可配置程序分析的静态分析的形式化体系进行扩展。首先提出了可配置程序分析的静态分析框架;之后说明了可配置程序分析在进行抽象解释时存在的可终止性问题;最后对可配置程序分析进行扩展,保证分析过程的可终止性。(2)说明了如何使用扩展的可配置程序分析并验证运行时错误。首先给出了从代码到程序控制流图的转化方法;之后配置相应参数完成抽象解释的分析过程,以求得不动点抽象值;最后根据不动点抽象值验证程序是否存在运行时错误。(3)设计实现了对运行时错误进行分析和验证的原型工具,并对航空器的襟缝翼控制系统进行分析。首先给出了基于扩展的可配置程序分析的原型工具设计思想;然后使用该原型工具对襟缝翼控制系统的部分代码进行分析;最后给出了该原型工具的分析结果,发现了襟缝翼控制系统中的运行时错误。