一句话：提出可从少量正样本高效推断的（合取）可解元组模式，并用于 CHC 求解器验证递归数据结构程序。
尽管自动化程序验证已有进展，全自动验证操作递归数据结构的程序仍很困难。本文提出可解元组模式（STP）与合取可解元组模式（CSTP），用于表达和推断类表递归数据结构之间的不变式。其显著特点是仅需少量正样本即可高效推断，无需负样本。作者给出 STP/CSTP 的性质与推断算法，并将 CSTP 推断集成到支持类表数据结构的 CHC（约束 Horn 子句）求解器中，作为自动化程序验证工具的统一后端。集成 (C)STP 推断的 CHC 求解器在 CHC-COMP 2025 的 ADT-LIN 赛道以显著优势夺冠。
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.
@article{paperbot3767,
title = {Solvable Tuple Patterns and Their Applications to Program Verification},
author = {Naoki Kobayashi and Ryosuke Sato and Ayumi Shinohara and Ryo Yoshinaka},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808258}
}