An overview of the mCRL2 modelling and verification toolset

• Jan Friso Groote, Eindhoven University of Technology, the Netherlands

mCRL2 is a process algebraic language to specify the behaviour of communicating systems. It allows to specify parallel behaviour with data, time and probabilities. It provides various behavioural reduction and visualisation algorithms to help understand behaviour. It uses the modal mu-calculus with data and time to specify properties. Both languages are restricted to their essential necessities, and mathematical elegance was more a driving factor in their design than user acceptance. But they are both extremely expressive and versatile. mCRL2 and its modal logic are very effective in modelling and analysing core protocols and distributed algorithms. But – due to its powerful algorithms – they are also used as the verification backend for various industrial software development environments. mCRL2 comes with the Boost license meaning that it is open source and free to use for any purpose, both commercially and researchwise.

Short biography

Jan Friso Groote  is a Full Professor and Chair of Formal Systems Analysis group in the Department of Mathematics and Computer Science at Eindhoven University of Technology (TU/e), and has been working at ASML part-time. His areas of expertise include Computer systems, architectures, software, algorithms, embedded systems and formal methods. Jan Friso has contributed to  structural operational semantics  and verification technology. He is the founding father of the process modeling language and analysis tool set  mCRL2. This tool set makes it possible to describe the behavior of software with data, time and probabilities, whilst proving properties related to this behavior, expressed in the modal mu-calculus, as well as reducing and visualizing this. His industrial experience shows that improvements to the verification techniques and algorithms, and the usage of software development styles suitable for verification reduce the development time with a factor three increasing the quality with a factor 10. Especially regarding the quality, it can be expected that substantial further improvements are possible, hopefully leading to zero defect software.

Challenges of a point & click mathematical proof builder interface

• Benoit Rognier, Edukera France

One of the key features of Edukera is the ergonomic design of the numerical paper which allows students to build a mathematical proof with point and click interactions. This numerical paper has been developed and improved over several years of experiment with students' and teachers' feedback. This session will address the key challenges a formal proof interface may pose:

• How to present a mathematical proof?
• Shall a proof assistant mimic the manual process?
• How to build a proof? Should it be like developing code or should it be with point & click interactions?
• How to present a theory (set of theorems) and search in it?
• How to conduct calculations?
• How to deal with obvious deductive arguments?

This session will show the experiments that have been conducted over the years and their outcomes.

The company

Edukera, created in 2014, has developed an online educational application to teach mathematics that relies on the use of the formal proof assistant Coq (developed by Inria).

Since its commercial launch in 2016, the Edukera application has been used with success in several universities by 8,500 students who have solved over half a million exercises.