Algorithmic Verification of Continuous and Hybrid Systems
  We provide a tutorial introduction to reachability computation, a class of computational techniques that exports verification technology toward continuous and hybrid systems. For open under-determined systems, this technique can sometimes replace an infinite number of simulations. 
Oded Maler (CNRS-VERIMAG)
cs.SY cs.FL cs.LO cs.NA