Despite the recent progress of automated program verification techniques, fully automated verification of programs manipulating recursive data structures remains a challenge. We introduce solvable tuple patterns (STPs) and conjunctive STPs (CSTPs), novel formalisms for expressing and inferring invariants between list-like recursive data structures. A distinguishing feature of STPs is that they can be efficiently inferred from only a small number of positive samples; no negative samples are required. After presenting properties and inference algorithms of STPs and CSTPs, we show how to incorporate the CSTP inference into a CHC (Constrained Horn Clauses) solver supporting list-like data structures, which serves as a uniform backend for automated program verification tools. A CHC solver incorporating the (C)STP inference has won the ADT-LIN category of CHC-COMP 2025 by a significant margin.

翻译：尽管近期自动程序验证技术取得了进展，但操作递归数据结构的程序的完全自动验证仍是一项挑战。我们引入了可解元组模式（STP）和合取可解元组模式（CSTP），这是用于表达和推断类列表递归数据结构之间不变量的新颖形式化方法。STP的一个显著特征是只需少量正样本即可高效推断，无需负样本。在介绍STP和CSTP的性质及推断算法后，我们展示了如何将CSTP推断集成到支持类列表数据结构的CHC（约束Horn子句）求解器中，该求解器作为自动程序验证工具的统一后端。集成了（C）STP推断的CHC求解器在CHC-COMP 2025的ADT-LIN类别中以显著优势夺冠。