随着程序员和用户对计算机系统软件和可执行程序安全性和正确性的要求不断提高，程序验证以其可靠而高精确的验证结果，在计算机领域已经越来越受欢迎。验证一个程序具体是指使用正规的数学方法，证明该段程序满足特定的由其规范描述的属性。近年来，为了使得被验证程序的正确性不依赖于庞大复杂的编译器的正确性，越来越多的程序验证工作选择直接在机器语言或者汇编语言上进行。然而，验证汇编程序具有很大的困难，因为汇编语言不具备高级语言中的非常清晰的抽象机制的结构（如循环体结构、函数结构等），来帮助程序的理解和验证。在汇编语言中，仅有的结构为由一连串顺序指令组成以跳转指令结尾的程序代码的基本块。因为缺乏结构化的抽象机制，为了能够一致地验证各种抽象机制，已有的汇编语言级程序验证系统只能选择忽略所有的抽象机制，使用基本块作为验证的基本单元，将所有的程序代码都以延续传递风格（Continuation Passing Style，简称CPS）来理解和验证。因为对程序中抽象机制意义的破坏，CPS风格的验证系统很难能够被用来验证大的软件系统。另外，CPS逻辑验证系统一般仅能够验证汇编程序的安全性，却很难保证它们的部分正确性。本文提出了上述问题的解决方法，其主要内容及贡献包括：本文提出了一个验证汇编程序的新方法。该方法能够直接在汇编级验证程序的部分正确性而不丢失对程序原有机制的理解。原有汇编级程序验证系统的程序验证步骤为：首先直接在汇编程序实际代码上为每个基本块提供规范，之后使用系统的推理规则进行验证。在本文的提出的方法中，我们引入显式控制流语言CFEL（Control-Flow-Explicit Language的简写）这个介于程序规范和汇编程序实际代码之间的辅助结构。顾名思义，我们使用CFEL来描述程序的控制流，并在验证时使用控制流来代表程序本身。CFEL结构简单却具有强大的表达力，能够描述包括函数调用和返回、异常处理、嵌入代码指针、自修改代码等各种程序机制的控制流。在一个程序实际被验证前，我们首先通过使用CFEL描述各段程序的控制流来辅助程序的验证。而验证所需要的规范将会直接提供给CFEL描述的控制流段。在CFEL的基础上，我们提供的一套结构简单、模块化并且适用性广的具体验证系统TCAP（Trail-Based Certifying Assembly Programming的简写）。TCAP的推理规则用来保证CFEL描述的各个控制流块确实是实际程序的正确控制流，并且各个控制流块的执行特性满足所提供的规范。带有各种不同程序抽象机制的汇编程序可以在TCAP这一个验证系统中验证，不需要使用不同系统对各个不同的抽象机制进行验证后将证明想办法链接在一起。因为CFEL已经描述了程序的控制流信息，TCAP中的规范以及规则都相对简单和易用。本文还提供一些使用TCAP来验证具有各种抽象机制的实际程序的例子。本文为TCAP提供了一套基于步指标的语义模型。其中步指标指的是程序关心的需要保证安全的程序执行步数。为一套支持多重程序抽象机制的验证系统提供语义模型是相当困难的工作，很多汇编级验证系统也因此选择使用语法的方法来证明其可靠性。语义模型为验证系统的推理规则定义具体的意义，从而使得系统更易扩展。另外，相比于语法方法，语义方法的模块性和泛型性也是其非常重要的优势之一，为验证系统提供一个简单易懂的语义模型已经成为计算机理论中很多重要研究工作的主要内容。本文中提供的语义模型简单易懂却不失强大的表达力。整个语义模型基于简单而直观的带有步指标的操作语义而不需要任何复杂理论，却可以解释支持包括嵌入代码指针在内的大量程序抽象机制的验证系统，稍微扩展后甚至可以支持高阶框架规则。而与潜入代码指针机制结合的高阶框架规则的语义支持是目前局部验证领域中的公认难点问题之一。