We survey a broad line of research concerned with the application of concepts and techniques from formal verification to the model checking of reactive systems and of dynamical models, and to the synthesis of strategies for control objectives. The models and techniques discussed in this contribution are of interest to the research area concerned with heterogeneous models and are of relevance for applications dealing with cyber-physical systems. The models under consideration encompass differences in state/variable type—finite vs. (un-)countably infinite—and in model semantics—(non-)deterministic vs. probabilistic. We categorise the discussed techniques into two main approaches: on the one hand, the derivation and use of formal abstractions; and on the other, the synthesis of certificates. We also distinguish between the separate-yet-related objectives of model checking and of strategy synthesis.