{"ID":2876962,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2508.20365","arxiv_id":"2508.20365","title":"Solvable Tuple Patterns and Their Applications to Program Verification","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.","short_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-l...","url_abs":"https://arxiv.org/abs/2508.20365","url_pdf":"https://arxiv.org/pdf/2508.20365v3","authors":"[\"Naoki Kobayashi\",\"Ryosuke Sato\",\"Ayumi Shinohara\",\"Ryo Yoshinaka\"]","published":"2025-08-28T02:30:02Z","proceeding":"cs.PL","tasks":"[\"cs.PL\"]","methods":"[]","has_code":false}