Soonho Kong

An Efficient Delta-decision Procedure Degree Type: Ph.D. in Computer Science
Advisor(s): Edmund M. Clarke, Randal E. Bryant
Graduated: May 2023

Abstract:

Delta-complete analysis demonstrates the decidability and complexity of delta-complete decision procedures through appropriate relaxations of exact decision problems. This framework presents a potential for addressing various practical problems in science and engineering involving high-order polynomials, transcendental functions, and ordinary differential equations. However, significant challenges remain in the development of viable and practical delta-decision procedures. This dissertation aims to address the challenge of designing and implementing a scalable delta-decision procedure that incorporates rich theories and support for quantifiers, as well as a bounded reachability analysis tool that is based on such a procedure.

First, we propose algorithms for solving SMT problems that involve ordinary differential equations (ODEs) by utilizing ODE constraints to design pruning operators within a branch-and-prune framework. Furthermore, we prove the delta-completeness of our algorithms.

Second, we present algorithms for solving SMT problems that involve universal quantification and a broad range of nonlinear functions by integrating interval constraint propagation, counterexample-guided synthesis, and numerical optimization. The proposed algorithms are demonstrated to be effective in handling a wide range of challenging global optimization and control synthesis problems.

Finally, we present dReal and dReach, a delta-SMT solver and a delta-reachability analysis tool respectively, for nonlinear real formulas and hybrid systems. dReal is capable of handling various nonlinear real functions, such as polynomials, trigonometric functions, and exponential functions, and implements the delta-complete decision procedure framework. dReach, on the other hand, encodes reachability problems as first-order real formulas and solves them using dReal. As a result, dReach is equipped to handle a wide range of highly nonlinear hybrid systems, as demonstrated by its scalability on various realistic models from biomedical and robotics applications.

Thesis Committee:
Edmund M. Clarke (Co-Chair)
Randal E. Bryant (Co-Chair)
Jeremy Avigad
Marijn J.H. Heule
Leonardo de Moura (Amazon Web Services)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Keywords:
Satisfiability Modulo Theory, Ordinary Differential Equations, Decision Procedures, Delta-decidability, Hybrid Systems, Reachability, Numerical Optimization, Bounded Model Checking