# Solvable Tuple Patterns and Their Applications to Program Verification

## TL;DR

This paper introduces solvable tuple patterns (STPs) and conjunctive STPs (CSTPs), novel tools for inferring invariants in recursive data structures, significantly advancing automated program verification capabilities.

## Contribution

It presents the formalism, inference algorithms, and integration of STPs and CSTPs into a CHC solver, improving verification of recursive data structures.

## Key findings

- CSTP inference can be efficiently derived from positive samples only.
- Incorporating CSTPs into a CHC solver enhances verification of list-like data structures.
- The solver won the ADT-LIN category of CHC-COMP 2025 by a large margin.

## 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.