An Efficient Delta-decision Procedure

 Delta-complete analysis demonstrates the decidability and complex-
ity of delta-complete decision procedures through appropriate relax-
ations 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 ordi-
nary 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 exponen-
tial 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.