| 基于SAT求解的面向对象程序类型分析 |
| |
| 引用本文： | 曹璟,徐宝文.基于SAT求解的面向对象程序类型分析[J].计算机科学,2009,36(1):256-262. |
| |
| 作者姓名： | 曹璟 徐宝文 |
| |
| 作者单位： | 1. 东南大学计算机科学与工程学院南京,210096
2. 江苏软件质量研究所南京,210096 |
| |
| 基金项目： | 国家杰出青年科学基金，国家自然科学基金与微软亚洲研究院联合资助项目，国家自然科学基金，江苏省自然科学基金，江苏省高技术研究项目 |
| |
| 摘 要： | 类型分析是面向对象程序分析中的重要环节,精确的类型分析能够提高其它程序分析的精度.由于传统精确分析方法固有的高复杂性,现有的类型分析大都使用粗糙的分析方法.提出了一种基于SAT求解的面向对象程序类型分析方法.该方法用命题逻辑表示类型在变量间的传递关系,将程序抽象成命题公式,并使用高效的SAT求解器求解,从而获得变量运行时的类型集合.该方法是流敏感的,并且具有良好的伸缩性,既可以进行快速但精度低的上下文不敏感分析,也可以进行较慢但精度高的上下文敏感分析.
|
| 关 键 词： | 命题公式可满足性验证 类型分析 程序分析 面向对象程序 |
| 收稿时间： | 2008/2/21 0:00:00 |
Object-oriented Program Type Analysis Based on SAT Solver |
| |
| CAO Jing,XU Bao-wen.Object-oriented Program Type Analysis Based on SAT Solver[J].Computer Science,2009,36(1):256-262. |
| |
| Authors: | CAO Jing XU Bao-wen |
| |
| Affiliation: | Department of Computer Science & Engineering;Southeast University;Nanjing 210096;China;Jiangsu Institute of Software Quality;China |
| |
| 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 but coarse analyses.This paper presented a new type analysis method of object-oriented program based on SAT solver,in which we show transfer relationship among variables by the proposition logic method,abstract programs into proposition formulas and adopt highl... |
| |
| Keywords: | Type analysis SAT Program analysis Object-oriented programming |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
