| 基于抽象解释理论的程序验证技术 |
| |
| 作者姓名： | 李梦君 李舟军 陈火旺 |
| |
| 作者单位： | 国防科学技术大学,计算机学院,湖南,长沙,410073;北京航空航天大学,计算机科学与工程学院,北京,100083 |
| |
| 基金项目： | Supported by the National Natural Science Foundation of Chinaunder GrantNos.60473057,90604007(国家自然科学基金) |
| |
| 摘 要： | 抽象解释(abstract interpretation)理论是Cousot.P和Cousot.R于1977年提出的程序静态分析时构造和逼近(approxiamation)程序不动点语义的理论.描述了程序语义基于Galois连接的抽象解释理论框架,讨论了基于抽象解释理论的程序变换、程序安全性验证和活性性质验证这3种典型的应用,并指出了基于抽象解释理论的程序验证的主要研究方向.
|
| 关 键 词： | 抽象解释理论 Galois连接 程序验证 |
| 收稿时间： | 2006-11-14 |
| 修稿时间： | 2007-04-25 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载免费的PDF全文 |
|
