43 citations · 81 across the 16 of their papers we have counts for
Showing 2012Show all
2 papers · 1 filter
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…