Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation
Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation
复制标题
使用用于测试输入生成的分离逻辑增强基于堆的程序的符号执行
DOI：
10.1007/978-3-030-31784-3_12
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
S. Qin
中科院分区：
文献类型：
--
作者：
Long H. Pham;Quang Loc Le;Quoc;Jun Sun;S. Qin
符号执行是一种成熟的测试输入生成方法。尽管在数值领域取得了巨大的成功，但由于缺乏对无界堆上的符号值的简洁和精确的描述，基于堆的程序的现有符号执行技术仍然受到限制。在这项工作中，我们提出了一种基于分离逻辑的基于堆的程序的新符号执行方法。我们提案的本质是上下文相关的延迟初始化，这是一种有效生成测试输入的新颖方法。我们的方法与现有方法有两个不同之处。首先，我们的方法基于分离逻辑，这使我们能够精确捕获基于堆的程序的先决条件，从而避免生成无效的测试输入。其次，我们仅生成完全初始化的测试输入，与最先进的工具生成的部分初始化的测试输入相比，这在实践中更有用。我们已经将我们的方法实现为一个名为 Java StarFinder 的工具，并在一组具有复杂堆输入的程序上对其进行了评估。结果表明，我们的方法显着减少了无效测试输入的数量并提高了测试覆盖率。
Symbolic execution is a well established method for test input generation. Despite of having achieved tremendous success over numerical domains, existing symbolic execution techniques for heap-based programs are limited due to the lack of a succinct and precise description for symbolic values over unbounded heaps. In this work, we present a new symbolic execution method for heap-based programs based on separation logic. The essence of our proposal is context-sensitive lazy initialization, a novel approach for efficient test input generation. Our approach differs from existing approaches in two ways. Firstly, our approach is based on separation logic, which allows us to precisely capture preconditions of heap-based programs so that we avoid generating invalid test inputs. Secondly, we generate only fully initialized test inputs, which are more useful in practice compared to those partially initialized test inputs generated by the state-of-the-art tools. We have implemented our approach as a tool, called Java StarFinder, and evaluated it on a set of programs with complex heap inputs. The results show that our approach significantly reduces the number of invalid test inputs and improves the test coverage.
DOI：
10.1016/j.scico.2010.07.004
发表时间：
2012-08
期刊：
Sci. Comput. Program.
影响因子：
--
作者：
W. Chin;C. David;Huu Hai Nguyen;S. Qin
通讯作者：
W. Chin;C. David;Huu Hai Nguyen;S. Qin
将符号执行和基于搜索的测试相结合，对具有复杂堆输入的程序进行测试
DOI：
10.1145/3092703.3092715
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Braione P
通讯作者：
Braione P
影响因子：
2.5
作者：
Calcagno, Cristiano;Distefano, Dino;Yang, Hongseok
通讯作者：
Yang, Hongseok