  Hybrid systems exhibit both continuous and discrete behavior. Analyzing
hybrid systems is known to be hard. Inspired by the idea of concolic testing
(of programs), we investigate whether we can combine random sampling and
symbolic execution in order to effectively verify hybrid systems. We identify a
sufficient condition under which such a combination is more effective than
random sampling. Furthermore, we analyze different strategies of combining
random sampling and symbolic execution and propose an algorithm which allows us
to dynamically switch between them so as to reduce the overall cost. Our method
has been implemented as a web-based checker named HyChecker. HyChecker has been
evaluated with benchmark hybrid systems and a water treatment system in order
to test its effectiveness.
