基于抽象解释理论的程序验证技术
Program Verification Techniques Based on the Abstract Interpretation Theory作者机构：国防科学技术大学计算机学院湖南长沙410073 北京航空航天大学计算机科学与工程学院北京100083
出 版 物：《软件学报》 (Journal of Software)
年 卷 期：2008年第19卷第1期
页 面：17-26页
核心收录：
学科分类：08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论]
基 金：Supported by the National Natural Science Foundation of Chinaunder GrantNos.60473057 90604007(国家自然科学基金)
摘 要：抽象解释(abstract interpretation)理论是Cousot.P和Cousot.R于1977年提出的程序静态分析时构造和逼近(approxiamation)程序不动点语义的理论.描述了程序语义基于Galois连接的抽象解释理论框架,讨论了基于抽象解释理论的程序变换、程序安全性验证和活性性质验证这3种典型的应用,并指出了基于抽象解释理论的程序验证的主要研究方向.
维普期刊数据库
同方期刊数据库