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

摘要：

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

关键词：命题公式可满足性验证、类型分析、程序分析、面向对象程序

所属期刊栏目：36

分类号：TP3;O14

资助基金：国家杰出青年科学基金项目60425206;国家自然科学基金与微软亚洲研究院联合资助项目60633010;国家自然科学基金项目60503033、60403016;江苏省自然科学基金项目BK2005060;江苏省高技术研究项目BG2005032

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

页数：共7页

页码：256-262