| 基于抽象解释理论的程序验证技术 |
| |
| 引用本文： | 李梦君,李舟军,陈火旺. 基于抽象解释理论的程序验证技术[J]. 软件学报, 2008, 19(1): 17-26. DOI: 10.3724/SP.J.1001.2008.00017 |
| |
| 作者姓名： | 李梦君 李舟军 陈火旺 |
| |
| 作者单位： | 国防科学技术大学,计算机学院,湖南,长沙,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 |
Program Verification Techniques Based on the Abstract Interpretation Theory |
| |
| LI Meng-Jun,LI Zhou-Jun and CHEN Huo-Wang. Program Verification Techniques Based on the Abstract Interpretation Theory[J]. Journal of Software, 2008, 19(1): 17-26. DOI: 10.3724/SP.J.1001.2008.00017 |
| |
| Authors: | LI Meng-Jun LI Zhou-Jun CHEN Huo-Wang |
| |
| Abstract: | |
| |
| Keywords: | abstract interpretation theory Galois connection program verification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
