I will review FDR3, the parallel implementation of the CSP refinement checker FDR, together with some of its approaches to the state explosion problem.  These include symmetry reduction, partial order reduction as well as improvements to its support for semantic-preserving compression.  I will also discuss a new approach to verification which I term "static model checking", using deadlock analysis as the motivating example.  I will also review the industrial uses of FDR and discuss our plans for building new technology for supporting model-based embedded software development