  Simulation and formal verification are important complementary techniques
necessary in high assurance model-based systems development. In order to
support coherent results, it is necessary to provide unifying semantics and
automation for both activities. In this paper we apply Interaction Trees in
Isabelle/HOL to produce a verification and simulation framework for state-rich
process languages. We develop the core theory and verification techniques for
Interaction Trees, use them to give a semantics to the CSP and Circus
languages, and formally link our new semantics with the failures-divergences
semantic model. We also show how the Isabelle code generator can be used to
generate verified executable simulations for reactive and concurrent programs.
