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

计算机科学 ›› 2009, Vol. 36 ›› Issue (1): 256-262.

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

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
本研究得到国家杰出青年科学基金项目（60425206）,国家自然科学基金与微软亚洲研究院联合资助项目（60633010）,国家自然科学基金项目（60503033、60403016）,江苏省自然科学基金项目（BK2005060）,江苏省高技术研究项目（BG2005032）资助.

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

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

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

Abstract: Type analysis plays an important role in object-oriented program analysis. Accurate type analysis will improve the precision of other program analyses. However, due to the inherent high complexity of traditional type analysis, people generally make rapid

Key words: Type analysis, SAT, Program analysis, Object oriented programming

. 基于SAT求解的面向对象程序类型分析[J]. 计算机科学, 2009, 36(1): 256-262. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed