VERIFICATION-INTEGRATED FALSIFICATION OF NON-DETERMINISTIC HYBRID SYSTEMS

This paper provides a method for coupling safety verification algorithms for non-deterministic (and, in general, non-linear) hybrid systems with the ability of finding concrete counterexamples, i.e., with falsification. Such a tight integration of verification with falsification has the advantage that verification attempts guide the search for concrete counterexamples, and endless attempts to verify unsafe systems or to find counterexamples in safe systems can often be avoided.