Mark Bouwman: Decompositional Branching Bisimulation Minimisation of Monolithic Processes
A well known technique to reduce the impact of the state space explosion problem problem is compositional minimisation. In this technique, first the state spaces of all components are computed and minimised modulo some behavioural equivalence (e.g., some form of bisimilarity). These minimised transition systems are subsequently combined to obtain the final state space. In …continue reading
Flip van Spaendonck: Efficient dynamic model based testing of models with run-to-completion semantics
Model based testing (MBT) provides an efficient and automated approach to finding discrepancies between software models and their implementation. If we want to incorporate MBT into the software development process, i.e. code changes are only accepted if the implementation remains in conformance with the model, then MBT must be able to thoroughly test the entire …continue reading
Nobuko Yoshida: mCRL2 for type-based verifications for distributed processes and programs
I first summarise how we used mCRL2 for checking properties of distributed processes and programs. I then talk about our most recent work which applies mCRL2 to unreliable systems, which we presented at CONCUR 2022.
Olav Bunte: Implementing OIL in Spoofax
In previous presentations about OIL I have mainly dived into its semantics, but in this presentation I’ll focus on its implementation in the Spoofax language workbench instead, which has been ongoing work for 5 years now. I’ll discuss how we tackled different implementation aspects of a language, such as syntax, transformations and static semantics, and evaluate …continue reading
Anton Wijs: GPU hash tables
Hash tables are important data structures for the fast storage and retrieval of data elements. They are, for instance, used often in explicit-state model checkers. In this talk I take a closer look at different types of hash tables, and address their suitability for use on graphics processors (GPUs). The current version of GPUexplore, an …continue reading
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