CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908620144246784 |
|---|---|
| author | Dobos-Kovács, Mihály Bajczi, Levente Vörös, András |
| author_facet | Dobos-Kovács, Mihály Bajczi, Levente Vörös, András |
| contents | Constrained Horn Clauses (CHCs) are widely adopted as intermediate representations for a variety of verification tasks, including safety checking, invariant synthesis, and interprocedural analysis. This paper introduces CHCVERIF, a portfolio-based CHC solver that adopts a software verification approach for solving CHCs. This approach enables us to reuse mature software verification tools to tackle CHC benchmarks, particularly those involving bitvectors and low-level semantics. Our evaluation shows that while the method enjoys only moderate success with linear integer arithmetic, it achieves modest success on bitvector benchmarks. Moreover, our results demonstrate the viability and potential of using software verification tools as backends for CHC solving, particularly when supported by a carefully constructed portfolio. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_26431 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses Dobos-Kovács, Mihály Bajczi, Levente Vörös, András Software Engineering Logic in Computer Science Programming Languages Constrained Horn Clauses (CHCs) are widely adopted as intermediate representations for a variety of verification tasks, including safety checking, invariant synthesis, and interprocedural analysis. This paper introduces CHCVERIF, a portfolio-based CHC solver that adopts a software verification approach for solving CHCs. This approach enables us to reuse mature software verification tools to tackle CHC benchmarks, particularly those involving bitvectors and low-level semantics. Our evaluation shows that while the method enjoys only moderate success with linear integer arithmetic, it achieves modest success on bitvector benchmarks. Moreover, our results demonstrate the viability and potential of using software verification tools as backends for CHC solving, particularly when supported by a carefully constructed portfolio. |
| title | CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses |
| topic | Software Engineering Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2510.26431 |