%0 Journal Article
%T 基于抽象解释理论的程序验证技术
%A 李梦君
%A 李舟军
%A 陈火旺
%J -
%D 2008
%X 抽象解释(abstract interpretation)理论是Cousot.P和Cousot.R于1977年提出的程序静态分析时构造和逼近(approxiamation)程序不动点语义的理论.描述了程序语义基于Galois连接的抽象解释理论框架,讨论了基于抽象解释理论的程序变换、程序安全性验证和活性性质验证这3种典型的应用,并指出了基于抽象解释理论的程序验证的主要研究方向
%K 抽象解释理论 Galois连接 程序验证
%U http://www.jos.org.cn/jos/ch/reader/view_abstract.aspx?file_no=20080103&flag=1