Solvable Tuple Patterns and Their Applications to Program Verification
For automated program verification tools, this work provides a novel formalism to infer invariants for list-like data structures, achieving state-of-the-art results in a solver competition.
The paper introduces solvable tuple patterns (STPs) and conjunctive STPs (CSTPs) for inferring invariants between list-like recursive data structures, enabling efficient inference from positive samples only. The approach, integrated into a CHC solver, won the ADT-LIN category of CHC-COMP 2025 by a significant margin.
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.