Allan van Hulst: The quest for the mythical 57-regular Moore graph
Since 1966 it is known that only four regular undirected graphs having diameter 2 and girth 5 can exist. The construction of three of these 5,2-Moore graphs is known but it is still an open problem whether the remaining candidate srg(3250,57,0,1) exists at all. I have developed an algorithm that constructs a partial solution to …continue reading
Rodin Aarssen: Concrete Syntax with Black Box Parsers
Meta programming is the art of writing software that takes source code as input for manipulation, analysis or code generation. Many meta programming systems reason about abstract syntax trees representing this source code, which requires intimate knowledge of the data type that describes the abstract syntax. Concrete syntax patterns allow meta programmers to create and perform matching on syntax trees using …continue reading
Wieger Wesselink: About the Design and Implementation of State Space Exploration in the mCRL2 toolset
An important use case of the mCRL2 tool set is state space exploration. An efficient and feature-rich implementation is available that works quite well in practice. Unfortunately the design of this implementation is quite complicated, and there is insufficient documentation. This makes it very hard to make any changes, or to add new functionality. During the …continue reading
Rick Erkens: “Rewriting the Term Rewriter Part 1: Introduction and Matching”
In an mCRL2 specification the user can specify processes with data, that can in turn be manipulated through the computational model of term rewriting. The term rewriter that the toolset uses now is reasonably fast and yet the bottleneck for state space generation is often found in the rewriter. This calls for optimizing this part …continue reading
Tim Willemse: Variability Parity Games
Parity games are two-player, infinite duration games that can be used answer whether a property holds true of a system with a yes or no. In several application domains, one is not only interested in a yes/no answer, but in computing some/all values to parameters in a system description for which a property holds true. …continue reading
Jurriaan Rot: Coalgebra Learning via Duality
Automata learning is a popular technique for inferring minimal automata through membership and equivalence queries. We generalise learning from automata to a large class of state-based systems, using the theory of coalgebras. The approach relies on the use of logical formulas as tests, based on a dual adjunction between states and logical theories. This allows …continue reading
Olav Bunte: “Formalising the semantics of OIL: the first steps”
In the last years an increasing number of companies have shown interest in applying verification techniques in model based software engineering and Océ is one of them. To apply such techniques it is necessary to have a formal semantics of the modelling language used, which in our case is OIL (Océ Interaction Language). We show …continue reading
Maurice Laveaux: Correct and Efficient Antichain Algorithms for Refinement Checking
Refinement checking plays an important role in system verification. This means that the correctness of the system is established by showing a refinement relation between two models; one for the implementation and one for the specification. Previously, Wang et al. presented an algorithm based on antichains to efficiently decide stable failures refinement and failures-divergences refinement. …continue reading
Thomas Neele: Verifying System-Wide Properties of Industrial Component-Based Software
Analytical Software Design (ASD) enables model-based development of component software systems. Until now, functional verification of ASD systems is only possible on a per-component basis. There is no functional verification engine for ASD itself, so this verification relies on a translation of individual components to mCRL2, a process-algebraic model checker. We show how to extend …continue reading
Alexander Fedotov: Fixing block and idle equations for FSMs in MaDL (work in progress)
The xMAS language introduced a convenient way of high-level modeling and verification of communication fabrics. For micro-architectural models expressed in xMAS, it was shown that the problem of proving liveness could be transformed into a SAT-problem, which is advantageous in terms of scalability. Later on, Verbeek et al. proposed an approach to combine basic xMAS …continue reading