基于抽象解释理论的程序验证技术

摘要：

抽象解释(abstract interpretation)理论是Cousot.P和Cousot.R于1977年提出的程序静态分析时构造和逼近(approxiamation)程序不动点语义的理论.描述了程序语义基于Galois连接的抽象解释理论框架,讨论了基于抽象解释理论的程序变换、程序安全性验证和活性性质验证这3种典型的应用,并指出了基于抽象解释理论的程序验证的主要研究方向.

关键词：抽象解释理论、Galois连接、程序验证

所属期刊栏目：19

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金60473057;90604007

在线出版日期：2008-05-14（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：17-26