TRI Author: Soonho Kong All Authors: Soonho Kong, Armando Solar-Lezama, Sicun Gao We propose δ-complete decision procedures for solving satisfiability of nonlinear SMT problems over real numbers that contain universal quantification and a wide range of nonlinear functions. The methods combine interval constraint propagation, counterexample-guided synthesis, and numerical optimization. In particular, we show how to handle the interleaving of numerical and symbolic computation to ensure delta-completeness in quantified reasoning. We demonstrate that the proposed algorithms can handle various challenging global optimization and control synthesis problems that are beyond the reach of existing solvers. Read more 

Citation: Kong, Soonho, Armando Solar-Lezama, and Sicun Gao. "Delta-decision procedures for exists-forall problems over the reals." In International Conference on Computer Aided Verification, pp. 219-235. Springer, Cham, 2018.