Computer Science Thesis Oral

April 27, 2023 9:00am — 11:00am

Location:
In Person - Gordon Bell Conference Room, Gates Hillman 5117

Speaker:
SOONHO KONG, Ph.D. Candidate, Computer Science Department, Carnegie Mellon University
https://soonhokong.github.io/

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, delta-SMT solver and 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:

Additional Information

Add event to Google
Add event to iCal