149 citations · 517 across the 29 of their papers we have counts for
Showing 2012 · cs.LOShow all
2 papers · 2 filters
cs.LO2012★ 11 cited
Delta-Decidability over the Reals
Sicun Gao, Jeremy Avigad, Edmund Clarke
Given any collection F of computable functions over the reals, we show that there exists an algorithm that, given any L_F-sentence φcontaining only bounded quantifiers, and any pos…
cs.LO2012★ 43 cited
Delta-Complete Decision Procedures for Satisfiability over the Reals
Sicun Gao, Jeremy Avigad, Edmund Clarke
We introduce the notion of "δ-complete decision procedures" for solving SMT problems over the real numbers, with the aim of handling a wide range of nonlinear functions including t…