## Ferry Timmers: Formalising Raking

Raking is a technique I have developed that allows extracting a statespace of software systems in situ. It does not query the system, but instead uses annotation of the system’s program code. In this talk, I will go deeper into the semantics of this technique.

## Rance Cleaveland: QUERY-CHECKING FOR FINITE LINEAR-TIME TEMPORAL LOGIC

This talk addresses the following problem: given a finite set of observations of system behavior, each observation itself being a finite sequence of system states, and a query consisting of a Finite LTL formula with missing subformulas, compute missing the missing subformulas that make the LTL formula true for all observations. This so-called query-checking problem *…continue reading*

## Tim Willemse: On Model-Based Testing

Model-Based Testing is a formal approach to testing (software) systems. Input-output conformance, often abbreviated by “ioco”, is one such approach to formal testing. It assumes that implementations can be modelled by input-enabled input-output transition systems, and it formalises when a given implementation conforms to a specification of that implementation. In the context of TNO-related projects, *…continue reading*

## Maurice Laveaux: Signature-based symbolic bisimulation minimisation

Symbolic exploration techniques allow us to construct symbolic state spaces with billions of states. Reducing these state spaces modulo (strong) bisimulation would help in further analysis. In this talk I will present a signature-based partition refinement algorithm from the literature to compute (strong) bisimulation on a symbolic state space. This algorithm requires a transformation of *…continue reading*

## Anna Stramaglia: A journey across Cordis models and their verification

In the MACHINAIDE project we verify Cordis models by means of mCRL2. Cordis models are UML-like models developed, tested and simulated in the Cordis SUITE. In this presentation I will take you along on our journey towards verification of Cordis models in three parts: Description of the structure and semantics of Cordis models Peculiarities in the *…continue reading*

## Hans Zantema: Passive automata learning: DFAs and NFAs

It is a natural question to find a DFA or NFA for which a given set of words should be accepted and another given set should not be accepted. In this presentation we investigate how to find a smallest automaton for both types by means of SMT solving, and compare the results.

## Jeroen Keiren: On the semantics of data types in mCRL2

In my previous talk I described the unfolding of process parameters in mCRL2, as it is done by lpsparunfold. This technique requires extending data specifications with new operations and equations. As part of the correctness, we need to reason about properties of the data specification. Working on these proofs triggered questions about the mCRL2 data *…continue reading*

## Jan Martens: Circular words, Fibonacci words and it’s implication on partition refinement algorithms for bisimilarity

In this talk we will consider deterministic finite automata(DFAs) with a singleton as alphabet. These rather restrictive machines have a strong connection with a very specific field of word combinatorics. In particular we will show how the periodicity of the bouncing DVD logo[1](or a billiard ball) is related to these automata and generate so-called Fibonacci words. *…continue reading*

## Tom Franken: Cole’s Parallel Merge Sort

In this talk, I shall explain Cole’s Parallel Merge Sorting Algorithm, which can sort lists of length n with O(n) processors in O(log n) time.

## Olav Bunte: The impact of the channel layout in asynchronous communication

During our work on the asynchronous communication of OIL components, we started to wonder what the impact would be of changing the communication model. In this presentation I will present our current findings. I will shortly explain related work from Engels, Mauw and Reniers on the hierarchy of communication models that served as the basis *…continue reading*