| Title | PyCHC: a Framework for Certified Horn Solving and CHC-based Design |
| Publication Type | Conference Paper |
| Year of Publication | 2026 |
| Authors | Becchi, Anna, Blicha Martin, Otoni Rodrigo, and Sharygina Natasha |
| Conference Name | CAV 2026 |
| Abstract | We present PyCHC, a solver-agnostic framework aimed at systems of constrained Horn clauses (CHC). PyCHC provides intuitive Python APIs to create and manipulate CHC systems programmatically and solve them using different backend solvers. Furthermore, PyCHC offers a certification pipeline to validate the correctness of results reported by the CHC solvers, via the use of independent satisfiability modulo theories (SMT) solvers and proof checkers. We present our framework's architecture and features, and demonstrate how it enables rapid prototyping of new CHC-based algorithms and experimentation with novel strategies for cooperative solving. We used PyCHC to validate the results of the Eldarica, Golem, and Spacer solvers on CHC-COMP benchmarks, finding several issues across different tool versions. |





