###
DOI:
Journal of Software:2008.19(1):17-26

基于抽象解释理论的程序验证技术
李梦君,李舟军,陈火旺
(国防科学技术大学 计算机学院,湖南 长沙 410073;北京航空航天大学 计算机科学与工程学院,北京 100083)
Program Verification Techniques Based on the Abstract Interpretation Theory
LI Meng-Jun,LI Zhou-Jun,CHEN Huo-Wang
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 8522   Download 6658
Received:November 14, 2006    Revised:April 25, 2007
> 中文摘要: 抽象解释(abstract interpretation)理论是Cousot.P和Cousot.R于1977年提出的程序静态分析时构造和逼近(approxiamation)程序不动点语义的理论.描述了程序语义基于Galois连接的抽象解释理论框架,讨论了基于抽象解释理论的程序变换、程序安全性验证和活性性质验证这3种典型的应用,并指出了基于抽象解释理论的程序验证的主要研究方向.
Abstract:The abstract interpretation theory was proposed by P. Cousot and R. Cousot in 1977, and is widely used in the program’s static analysis domain to construct and approximate the program’s fixpoint semantics. This paper describes the abstract interpretation framework of the program semantics based on the Galois connection, and then discusses three typical applications of the abstract interpretation theory: The program transformation, the program verification techniques about the safety property and the program verification techniques about the liveness property. Finally, it points out the main directions of the program verification techniques based on the abstract interpretation theory.
文章编号:     中图分类号:    文献标志码:
基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.60473057, 90604007 (国家自然科学基金) Supported by the National Natural Science Foundation of China under Grant Nos.60473057, 90604007 (国家自然科学基金)
Foundation items:
Reference text:

李梦君,李舟军,陈火旺.基于抽象解释理论的程序验证技术.软件学报,2008,19(1):17-26

LI Meng-Jun,LI Zhou-Jun,CHEN Huo-Wang.Program Verification Techniques Based on the Abstract Interpretation Theory.Journal of Software,2008,19(1):17-26