基于抽象解释理论的程序验证技术
, PP. 17-26
Keywords: 抽象解释理论,galois连接,程序验证
Abstract:
抽象解释(abstractinterpretation)理论是cousot.p和cousot.r于1977年提出的程序静态分析时构造和逼近(approxiamation)程序不动点语义的理论.描述了程序语义基于galois连接的抽象解释理论框架,讨论了基于抽象解释理论的程序变换、程序安全性验证和活性性质验证这3种典型的应用,并指出了基于抽象解释理论的程序验证的主要研究方向.
Full-Text
