基于SAT求解的面向对象程序类型分析

• 作者: 徐宝文 曹璟
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 命题公式可满足性验证 类型分析 程序分析 面向对象程序
• 年，卷（期）: 2009,（1）
• 所属期刊栏目: 软件工程
• 页码范围: 256-262
• 页数: 7页
• 分类号: TP3
• 字数: 9072字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-137X.2009.01.066

摘要

类型分析是面向对象程序分析中的重要环节,精确的类型分析能够提高其它程序分析的精度.由于传统精确分析方法固有的高复杂性,现有的类型分析大都使用粗糙的分析方法.提出了一种基于SAT求解的面向对象程序类型分析方法.该方法用命题逻辑表示类型在变量间的传递关系,将程序抽象成命题公式,并使用高效的SAT求解器求解,从而获得变量运行时的类型集合.该方法是流敏感的,并且具有良好的伸缩性,既可以进行快速但精度低的上下文不敏感分析,也可以进行较慢但精度高的上下文敏感分析.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	曹璟	东南大学计算机科学与工程学院	4	10	2.0	3.0
2	徐宝文		2	4	1.0	2.0