@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}
}
