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

• 作者: 李梦君 李舟军 陈火旺
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 抽象解释理论 Galois连接 程序验证
• 年，卷（期）: 2008,（1）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 17-26
• 页数: 10页
• 分类号: TP301
• 字数: 10859字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2008.00017

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李舟军	北京航空航天大学计算机科学与工程学院	136	2221	23.0	43.0
2	陈火旺	国防科学技术大学计算机学院	53	2116	23.0	45.0
3	李梦君	国防科学技术大学计算机学院	16	294	7.0	16.0