Modern programs usually 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. The paper of reseachers from the Programming Languages Lab - "Efficient Synthesis of Method Call Sequences for Test Generation and Bounded Verification" - proposes 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, the paper introduces 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 the proposed approach substantially outperforms the baselines in both test generation and bounded verification.
The authors of this paper are Yunfan Zhang (Ph.D. student), Ruidong Zhu (undergraduate student), Prof. Yingfei Xiong, and Prof. Tao Xie.