Milner initiated process algebras to describe and study the behaviour of interacting systems. Various people added modal logics to denote properties using which this behaviour can be studied. We brought these together in the language/toolset mCRL2 on which we have been working for more than 30 years now. The result is an abstract, but versatile modelling and analysis formalism, which we are using to develop and analyse distributed and parallel algorithms, solve behavioural puzzles, check communication protocols and produce software. The mCRL2 toolset has been adopted by a number of companies as verification backend. Multiple companies in the region around Eindhoven develop substantial parts of their software through verified models and some have literally many thousands of them. In this talk I will explain behavioural modelling and analysis via mCRL2, guided via a number of examples, and hope to convince you why I believe that process algebras and modal logics are utterly effective tools.
Join at http://imt.lu/seminar