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