Events at MetaForum MF 7.084

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

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

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

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

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

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

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

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