Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs
Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs
复制标题
用于分析面向对象程序的强属性的案例最优符号执行算法
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
J. Hatcliff
中科院分区：
文献类型：
--
作者：
Xianghua Deng;Robby;J. Hatcliff
最近的工作表明，符号执行技术可以作为正式分析的基础，能够自动检查针对强大界面规格的堆操作软件组件。在本文中，我们对面向对象的程序的现有符号执行算法提出了增强，这些算法可显着改善Bogor/Kiasan和JPF当前实施的算法。为了激励和证明在我们增强的方法中处理堆数据的新策略，我们对相关算法的性能进行了重要的经验研究，以及对堆形状的有趣案例计数分析，可以在几种广泛使用的Java数据结构软件包中出现。
Recent work has demonstrated that symbolic execution techniques can serve as a basis for formal analysis capable of automatically checking heap-manipulating software components against strong interface specifications. In this paper, we present an enhancement to existing symbolic execution algorithms for object-oriented programs that significantly improves upon the algorithms currently implemented in Bogor/Kiasan and JPF. To motivate and justify the new strategy for handling heap data in our enhanced approach, we present a significant empirical study of the performance of related algorithms and an interesting case counting analysis of the heap shapes that can appear in several widely used Java data structure packages.