计算机程序正逐步影响到人类社会的方方面面。无论在互联网还是个人电脑上，计算机程序的安全问题日益严峻。然而现实世界中的程序并不尽如人意，病毒肆虐，网络攻击防不胜防。这些问题都源于程序中潜伏着许多错误，其中一个小的错误有可能会导致整个软件系统的崩溃。而在诸多关键的领域，例如核反应堆、航天飞机的控制系统等等，计算机程序的半点闪失都将带来不可计数的惨痛损失。在软件开发过程中使用形式化的方法是提高软件质量的途径。在众多的形式化方法中，程序的静态验证是一种非常可靠的方法。本文采用方法是在携带证明的代码的框架中静态地验证程序。所谓携带证明的代码是首先静态地验证代码的安全性，然后将这个验证的详细过程作为安全性证明附加在程序上。主机在运行程序前检查程序携带的安全性证明的正确性。如果安全性证明是正确的，那么说明程序满足主机的安全策略，可以安全地运行而不破坏主机上的软件系统。本文首先在一个简单的验证框架中定义了程序、抽象机器、抽象机器的操作语义、安全，还有一个用来静态验证程序的推理系统。此框架可以用来构造简单的携带证明的代码。然而与以前的许多相关研究一样，此框架不能很好地支持模块化的程序验证。现实中的大量程序通常使用模块化的开发方式，模块化的开发方式可以把一个复杂的程序分解为若干个小的模块，不同的模块分别被开发，最后这些模块可以被链接到一起从而构成完整的程序。模块性在软件工程方面占有重要的地位。程序静态验证也应该具备模块性，即不同模块的验证可以分别进行，然后链接成为完整的安全性证明。另一方面，一个程序的不同模块可能是不同风格的代码，难以使用同一种验证推理系统去验证所有的模块。本文在简单验证框架上进行扩展，使之支持模块化验证。在此模块化框架中不同的模块可以分开进行验证，并分别得到各自的安全性证明，模块在链接的同时安全性证明也被链接到一起，从而得到整个程序的安全性证明。而且此框架支持不同的模块使用不同的验证逻辑进行验证。框架的特点是采用一个抽象的程序推理系统，它支持良好的模块验证。多个验证推理系统可以被统一嵌入到这个抽象的程序推理系统中。通过采用这种方法，一个模块不管使用哪些推理系统进行验证，只要这个验证推理系统可以被嵌入到抽象层次上，那么这个模块的安全性证明就可以被转换成抽象的推理系统中的安全性证明。本文研究了如何将一个支持控制栈推理的验证推理系统(被称为SCAP)嵌入到验证框架中，并移植了一个已有的动态内存分配模块(newpair)。同时本文还研究了如何将一个类型化的验证推理系统(被称为TALP)嵌入到验证框架中，并验证了一个小的调用动态内存分配的模块(main)。最后本文介绍了如何将两个使用不同的推理系统验证的模块连同安全性证明链接到一起。本文还研究了框架中的各个模块的安全性证明产生的自动性问题。本文不仅提出了验证推理系统SCAP中的验证条件生成器，而且提出了验证推理系统TALP的类型检查器。通过验证条件生成器与类型检查器的可靠性证明，模块的安全性证明的构造过程被大大简化，有利于验证规模较大的模块。文中所有的形式化定义，形式化描述以及证明都已使用的定理辅助证明工具Coq实现。因此所有的证明，包括框架的性质证明，示例程序的安全性证明的正确性可以使用机器自动检查。本文的工作虽然是对模块化验证框架的研究的初步探索，但是本文中的验证框架所表现出的良好的模块性为大规模程序的安全性验证带来良好的应用和研究前景。