Solvable Tuple Patterns and Their Applications to Program Verification
Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka
TL;DR
The paper tackles automated verification of programs manipulating list-like ADTs by introducing solvable tuple patterns (STPs) and conjunctive STPs (CSTPs) that can be learned from positive samples. It develops a formal inference framework with TPinf and CSTPinf, proves soundness, completeness (for STPs), and learnability, and shows decidability for CSTP-models of CHCs on words. It then integrates CSTP inference into CHC solving via CHoCoL and demonstrates strong empirical performance on CHC-COMP 2025 benchmarks, outperforming prior solvers and benefiting from a tight coupling with arithmetic reasoning through length abstraction. The work also extends to multisets/sets and provides a usable toolchain, TupInf, for STP/CSTP inference and CHCoL for CHC solving, highlighting its practical impact on automated verification of list-manipulating programs and suggesting future extensions to trees and broader language classes.
Abstract
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.