He contributed to structural operational semantics and verification technology. His particular contributions include the tyft/tyxt format for operational rules, the first algorithm to determine branching bisimulation and the cones and foci method to prove correctness of protocols and distributed algorithms. He is the founding godfather of the process modelling language and analysis tool sets μCRL and mCRL2.