%0 Journal Article
%T 基于sat求解的面向对象程序类型分析
%J 计算机科学
%D 2009
%X 类型分析是面向对象程序分析中的重要环节，精确的类型分析能够提高其它程序分析的精度。由于传统精确分析方法固有的高复杂性，现有的类型分析大都使用粗糙的分析方法。提出了一种基于sat求解的面向对象程序类型分析方法。该方法用命题逻辑表示类型在变量间的传递关系，将程序抽象成命题公式，并使用高效的sat求解器求解，从而获得变量运行时的类型集合。该方法是流敏感的，并且具有良好的伸缩性，既可以进行快速但精度低的上下文不敏感分析，也可以进行较慢但精度高的上下文敏感分析。
%K 命题公式可满足性验证类型分析程序分析面向对象程序
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=29209336&flag=1