Title: The mCRL2 behavioural specification language and tools, including new developments

Speaker: Prof. Jan Friso Groote, Technical University Eindhoven

Venue: Room 334, Building 5, Institute of Software, CAS

Time: Thursday May 30, 15:00

Abstract: The mCRL2 language originated in 1990 to specify communicating systems including data and time in a process algebraic style. Behavioural properties can be denoted using the modal mu-calculus with data and time, as it stands the most expressive logic for this purpose. The language and the logic have been provided with a complete mathematical underpinning, as well with a powerful toolset for analysis purposes. The tools are open source and free for use (www.mcrl2.org).

　　In this talk a short overview will be given of the language, its capabilities and its increasingly widespread use. Furthermore, some of the new developments will be addressed, namely probabilities, counterexamples/witnesses for arbitrarily complex behaviour properties and its use to verify global properties of newly developed industrial software.

Bio: Jan Friso Groote obtained a PhD at CWI and the University of Amsterdam in the area of operational semantics and process algebra in 1991. Since 1998, he works as a full professor at Eindhoven University of Technology. His main interest is in modelling and analysis of especially embedded software, with a focus on delivering correct efficiently. He is the father of the mCRL2 language and toolset.