Computer Science Thesis Proposal

Thursday, April 28, 2016 - 1:00pm


3002 Newell-Simon Hall


SOONHO KONG, Ph.D. Student

For More Information, Contact:

By allowing an appropriate relaxation to the exact decision problems, the delta-complete analysis showed the decidability and complexity results of delta-complete decision procedures. This framework opens a possibility of handling many interesting and practical problems occurring in science and engineering which contain higher-order polynomials, transcendental functions, and ordinary differential equations (ODEs). However, there is a big gap between this theoretical possibility and the realization of scalable and practically usable delta-decision procedures. This thesis aims to show the steps that are taken towards filling in this gap with convincing and practical examples showing the broad applicability of these procedures. In this thesis, we present the design and implementation of a delta complete decision procedure, dReal. Specifically, we address the following research problems to make the solver more efficient and practical. •We propose algorithms for solving delta-decision problems with ordinary differential equations. The algorithms use ODE constraints to design pruning operators in a branch-and-prune framework. They handle both standard decision problems with only existentially quantified variables, as well as a special case of exists-forall formulas which has universal quantifications over time variables. We show that the algorithms are delta-complete.  •We propose a new branch-and-prune framework that exploits the full power of SAT solving for exploring the search space with minimal overhead. This improvement is achieved by the generalization of pruning results and learning of new constraints. •We propose an algorithm to handle first-order formulas with one alternation of quantifier blocks in the delta-complete analysis framework. The algorithm is based on the idea of counterexample-guided refinement. For an exist-forall formula  φ = ∃x.∀y.f(x, y) , it searches for a counterexample  x = a  and  y = b  such that   ƒ(a, b)  does not hold. If such a counterexample is found, the algorithm uses y = b to guide a search on existentially quantified variable x by solving a partially instantiated constraint  ∃x.f(x, b) . We show that this method can handle various nonlinear global optimization problems found in the literature. We show that the above techniques help tackle the instances from real-world applications including bounded model-checking for hybrid systems and nonlinear global optimization problems. Thesis Committee: Edmund M. Clarke (Chair)Randal E. Bryant Jeremy Avigad Leonardo de Moura (Microsoft Research) Thesis Summary


Thesis Proposal