  We present the framework of delta-complete analysis for bounded reachability
problems of general hybrid systems. We perform bounded reachability checking
through solving delta-decision problems over the reals. The techniques take
into account of robustness properties of the systems under numerical
perturbations. We prove that the verification problems become much more
mathematically tractable in this new framework. Our implementation of the
techniques, an open-source tool dReach, scales well on several highly nonlinear
hybrid system models that arise in biomedical and robotics applications.
