Thursday, April 27, 2023, 9am

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:
Randal E. Bryant (Co-Chair)
Edmund M. Clarke (Co-Chair)
Jeremy Avigad
Marijn J.H. Heule
Leonardo de Moura (Amazon Web Services)

Additional Information

Event Type: Thesis Orals
Room Number: In Person
Building: Gordon Bell Conference Room, Gates Hillman 5117
Speaker's Name: SOONHO KONG
Speaker Website: soonhokong.github.io
Speaker's Professional Title: Ph.D. Candidate, Computer Science Department, Carnegie Mellon University
Talk Title: Efficient Delta-decision Procedure
Event Poster Title: Poster
Event Poster URL: www.cs.cmu.edu…
For More Information: jennsbl@cs.cmu.edu | deb@cs.cmu.edu
Affiliations: Computer Science Department (CSD)
Organization(s): SCS