现代程序经常需要操作基于堆的数据结构来执行计算。当为这些程序进行测试生成或有界验证时，我们往往需要确定是否存在满足给定规约的可达堆状态，以及通过对公有方法的一系列调用来构造出这个堆状态。由于公有方法和它们的调用参数共同形成的状态空间巨大，现有的方法通常采用静态分析或启发式搜索，希望只探索搜索空间的一小部分就能找到目标状态和目标调用序列。然而，这些方法在许多实际的复杂方法和规约面前没有令人满意的性能。本研究室论文《Efficient Synthesis of Method Call Sequences for Test Generation and Bounded Verification》提出了一种高效的方法调用序列合成算法，它包括一个用于探索给定范围内所有可达堆状态的离线过程，以及一个根据已探索的堆状态来生成方法调用序列以满足给定规约的在线过程。为了提高状态探索的效率，论文引入了抽象堆状态的概念用于紧凑地表示具有相同结构的多个堆状态，并提出了一种合并同构堆状态的策略。实验结果表明，论文提出的方法在测试生成和有界验证方面都大大优于参照方法。
研究室博士生张云帆是该论文的第一作者，熊英飞副教授是论文的通讯作者，其他作者包括北京大学本科生朱睿冬和北京大学谢涛教授。