Verification-Integrated Falsification of Non-Deterministic Hybrid Systems

Abstract

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.

Jan-Georg Smaus

Last modified: Wed Sep 15 13:15:58 MEST 2004