Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909709156483072 |
|---|---|
| author | Katsura, Hiroyuki Kobayashi, Naoki Sakayori, Ken Sato, Ryosuke |
| author_facet | Katsura, Hiroyuki Kobayashi, Naoki Sakayori, Ken Sato, Ryosuke |
| contents | We propose a novel approach to satisfiability checking of Constrained Horn Clauses (CHCs) over Algebraic Data Types (ADTs). CHC-based automated verification has gained considerable attention in recent years, leading to the development of various CHC solvers. However, existing solvers for CHCs over ADTs are not fully satisfactory, due to their limited ability to find and express models involving inductively defined functions/predicates (e.g., those about the sum of list elements). To address this limitation, we consider catamorphisms (generalized fold functions), and present a framework for automatically discovering appropriate catamorphisms on demand and using them to express a model of given CHCs. We have implemented a new CHC solver called Catalia based on the proposed method. Our experimental results for the CHC-COMP 2024 benchmark show that Catalia outperforms state-of-the-art solvers in solving satisfiable CHCs over ADTs. Catalia was also used as a core part of the tool called ChocoCatalia, which won the ADT-LIA category of CHC-COMP 2025. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_20726 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types Katsura, Hiroyuki Kobayashi, Naoki Sakayori, Ken Sato, Ryosuke Logic in Computer Science We propose a novel approach to satisfiability checking of Constrained Horn Clauses (CHCs) over Algebraic Data Types (ADTs). CHC-based automated verification has gained considerable attention in recent years, leading to the development of various CHC solvers. However, existing solvers for CHCs over ADTs are not fully satisfactory, due to their limited ability to find and express models involving inductively defined functions/predicates (e.g., those about the sum of list elements). To address this limitation, we consider catamorphisms (generalized fold functions), and present a framework for automatically discovering appropriate catamorphisms on demand and using them to express a model of given CHCs. We have implemented a new CHC solver called Catalia based on the proposed method. Our experimental results for the CHC-COMP 2024 benchmark show that Catalia outperforms state-of-the-art solvers in solving satisfiable CHCs over ADTs. Catalia was also used as a core part of the tool called ChocoCatalia, which won the ADT-LIA category of CHC-COMP 2025. |
| title | Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2507.20726 |