中文摘要：

近来在程序验证领域,Feng和Shao提出一个类Hoare逻辑的验证框架以验证包含中断的底层程序.在该工作基础上进行扩展,提出一个验证包含线程的动态创建和退出机制程序的框架.框架包含抽象机器模型、指令规范、逻辑推理系统、框架可靠性定理其证明.框架采用Hoare风格的推导方式,使用高阶逻辑描述指令的推理规则和安全策略,为证明带有线程的动态创建和退出的多线程程序的部分正确性提供了一种实用的方法.

英文摘要：

Recently Feng and Shao presented a Hoare-style framework for certifying low-level system programs involving hardware interrupts.On the base of this work,this paper presents an extended proof framework for verifying code with dynamic thread creation and termination.The extended framework including abstract machine model,formal specifications of instruction and logic reference rules,supports Hoare-logic style reasoning,and uses high-order logic to describe inference rules and security-policies.Our framework proposes a practical method for verifying the partial correctness of multithreaded programs.