Best paper award for Thomas Neele, Tim Willemse and Jan Friso Groote.
In October Thomas Neele presented during the 15th Conference of Format Aspects of Component Software the paper 'Solving parameterised Boolean equation systems with infinite data through quotienting' written together with Tim Willemse and Jan Friso Groote.
Parameterised Boolean Equation Systems (PBESs) can be used to represent many different kinds of decision problems. Most notably, model checking and equivalence problems can be encoded in a PBES. Traditional instantiation techniques cannot deal with PBESs with an infinite data domain. They propose an approach that can solve PBESs with infinite data by computing the bisimulation quotient of the underlying graph structure. Furthermore, they show how this technique can be improved by repeatedly searching for finite proofs. Unlike existing approaches, our technique is not restricted to subfragments of PBESs. Experimental results show that their ideas work well in practice and support a wider range of models and properties than state-of-the-art techniques.