@conference {424,
	title = { PyCHC: a Framework for Certified Horn Solving and CHC-based Design},
	booktitle = {CAV 2026},
	year = {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{\textquoteright}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.
},
	author = {Anna Becchi and Martin Blicha and Rodrigo Otoni and Natasha Sharygina}
}
@conference {417,
	title = {Syntactically Convex Model-Based Projection for Linear Real Arithmetic},
	booktitle = {TACAS 2026},
	year = {2026},
	abstract = {Quantifier elimination (QE) is a key task in formal verification algorithms,
and the ability to return partial results, such as under-approximations, is beneficial for many QE clients.
In Linear Real Arithmetic (LRA), existing QE methods often fail to preserve syntactic convexity,
that is, they return a disjunction even for a conjunctive input, or they return a large
non-minimal representation. We define the novel concept of Bidirectional Model-Based Projection
and a new QE algorithm for LRA (BMBP-QE) that
(i) returns a conjunctive over-approximation and a disjunctive under-approximation when interrupted early,
(ii) returns a minimal conjunction when the input is conjunctive, and
(iii) applies to arbitrary LRA formulae.
We show that BMBP-QE outperforms SMT-based QE algorithms,
offering improvements in both runtime and result size.},
	url = {https://link.springer.com/chapter/10.1007/978-3-032-22752-2_3},
	author = {Anna Becchi and Grigory Fedyukovich and Arie Gurfinkel and Lev Nachmanson}
}
