Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2508.20365 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910255873523712 |
|---|---|
| author | Kobayashi, Naoki Sato, Ryosuke Shinohara, Ayumi Yoshinaka, Ryo |
| author_facet | Kobayashi, Naoki Sato, Ryosuke Shinohara, Ayumi Yoshinaka, Ryo |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_20365 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Solvable Tuple Patterns and Their Applications to Program Verification Kobayashi, Naoki Sato, Ryosuke Shinohara, Ayumi Yoshinaka, Ryo Programming Languages 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. |
| title | Solvable Tuple Patterns and Their Applications to Program Verification |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2508.20365 |