| 验证带有线程的动态创建和退出的多线程程序 |
| |
| 引用本文： | 王海波,郭宇,陈意云.验证带有线程的动态创建和退出的多线程程序[J].小型微型计算机系统,2010,31(8). |
| |
| 作者姓名： | 王海波 郭宇 陈意云 |
| |
| 作者单位： | 中国科学技术大学,计算机科学与技术学院,安徽,合肥,230027;中国科学技术大学,苏州研究院,江苏,苏州,215123 |
| |
| 基金项目： | 国家自然科学基金项目，江苏省自然科学基金项目 |
| |
| 摘 要： | 近来在程序验证领域,Feng和Shao提出一个类Hoare逻辑的验证框架以验证包含中断的底层程序.在该工作基础上进行扩展,提出一个验证包含线程的动态创建和退出机制程序的框架.框架包含抽象机器模型、指令规范、逻辑推理系统、框架可靠性定理其证明.框架采用Hoare风格的推导方式,使用高阶逻辑描述指令的推理规则和安全策略,为证明带有线程的动态创建和退出的多线程程序的部分正确性提供了一种实用的方法.
|
| 关 键 词： | 程序验证 线程的动态创建和退出 多线程 汇编代码 |
Verifying Multithreaded Code with Dynamic Thread Creation and Termination |
| |
| WANG Hai-bo,GUO Yu,CHEN Yi-yun.Verifying Multithreaded Code with Dynamic Thread Creation and Termination[J].Mini-micro Systems,2010,31(8). |
| |
| Authors: | WANG Hai-bo GUO Yu CHEN Yi-yun |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
