一句话：提出基于抽象堆状态与同构状态合并的方法调用序列合成算法，高效生成满足规约的堆状态。
现代程序通常基于堆，测试生成与有界验证需要判定或构造满足给定规约的可达堆状态，并由公有方法调用序列实现。现有方法多采用静态分析或启发式搜索，仅探索搜索空间的一小部分，在复杂真实方法及规约上性能不理想。本文提出一种高效的方法调用序列合成算法，包括离线探索给定范围内所有可达堆状态的过程，以及从已探索堆状态在线生成满足规约的方法调用序列的过程。为提升状态探索效率，作者引入抽象堆状态来紧凑表示具有相同结构的堆状态，并提出合并结构同构状态的策略。实验结果表明，该方法在测试生成与有界验证任务上均显著优于基线方法。
Modern programs are usually heap-based, where the programs manipulate heap-based data structures to perform computations. In software engineering tasks such as test generation and bounded verification, we need to determine the existence of a reachable heap state that satisfies a given specification, or construct the heap state by a sequence of calls to the public methods. Given the huge space combined from the methods and their arguments, the existing approaches typically adopt static analysis or heuristic search to explore only a small part of search space in the hope of finding the target state and target call sequence early on. However, these approaches do not have satisfactory performance on many real-world complex methods and specifications. In this paper, we propose an efficient synthesis algorithm for method call sequences, including an offline procedure for exploring all reachable heap states within a scope, and an online procedure for generating a method call sequence from the explored heap states to satisfy the given specification. To improve the efficiency of state exploration, we introduce a notion of abstract heap state for compactly representing heap states of the same structure and propose a strategy of merging structurally-isomorphic states. The experimental results demonstrate that our approach substantially outperforms the baselines in both test generation and bounded verification.
@inproceedings{paperbot7299,
title = {Efficient Synthesis of Method Call Sequences for Test Generation and Bounded Verification},
author = {Yunfan Zhang and Ruidong Zhu and Yingfei Xiong and Tao Xie},
booktitle = {ASE},
year = {2022},
doi = {10.1145/3551349.3556951}
}