@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.},
	author = {Anna Becchi and Grigory Fedyukovich and Arie Gurfinkel and Lev Nachmanson}
}
@conference {405,
	title = {Validation of CHC Satisfiability with ATHENA},
	year = {2025},
	abstract = {Formal veriication tooling increasingly relies on logic solvers as automated reasoning engines. A commonality among these solvers is the high complexity of their codebases, which makes bug occurrence disturbingly frequent. Tool competitions have showcased many examples of state-of-the-art solvers disagreeing on the satisiability of logic formulas, be it solvers for Boolean satisiability (SAT), satisiability modulo theories (SMT), or constrained Horn clauses (CHC). The validation of solvers{\textquoteright} results is thus of paramount importance, in order to increase the conidence not only in the solvers themselves, but also in the tooling which they underpin. Among the formalisms commonly used by modern veriication tools, CHC is one that has seen, at the same time, extensive practical usage and very little eforts in result validation. We propose a two-layered validation approach for witnesses of CHC satisiability that validates CHC models via proof-backed SMT queries. We developed a modular evaluation framework, ATHENA, and assessed the approach{\textquoteright}s viability via large scale experimentation, comparing three CHC solvers, ive SMT solvers, and ive proof checkers. Our results indicate that the approach is feasible, with potential to be incorporated into CHC-based tooling, and also conirm the need for validation, with fourteen bugs being found in the tools used.},
	url = {https://dl.acm.org/doi/10.1145/3716505},
	author = {Otoni Rodrigo and Blicha Martin and Eugster Patrick and Sharygina Natasha}
}
