Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. We propose POR techniques that are sound for parity games, a well-established formalism for solving a variety of decision problems. As a consequence, we obtain the first POR method that is sound for model checking for the full modal mu-calculus. Our …continue reading

We present a methodology for generating a characterization of the memory used by an assembly program, as well as a formal proof that the assembly is bounded to the generated memory regions. A formal proof of memory usage is required for compositional reasoning over assembly programs. Moreover, it can be used to prove low-level security …continue reading

In this talk, I will discuss our recent experiences with using the mCRL2 toolset – which has a process-algebra based modelling language, a modal mu-calculus-based property language, and an explicit-state model checker – to support two major innovation activities from railway infrastructure managers. First, there is the EULYNX initiative of the European railway infrastructure managers. …continue reading