  We present an algorithm that quickly finds falsifying inputs for hybrid
systems, i.e., inputs that steer the system towards violation of a given
temporal logic requirement. Our method is based on a probabilistically directed
search of an increasingly fine grained spatial and temporal discretization of
the input space. A key feature is that it adapts to the difficulty of a problem
at hand, specifically to the local complexity of each input segment, as needed
for falsification. In experiments with standard benchmarks, our approach
consistently outperforms existing techniques by a significant margin. In
recognition of the way it works and to distinguish it from previous work, we
describe our method as a "Las Vegas tree search".
