Tom Franken: Autonomous Data Language for Parallel Programming
In this presentation, I shall introduce Autonomous Data Language, highlight its most important attributes and explain the main concepts of the language using some examples.
Valentina Castiglioni: Uncertainties, adaptability, and verification
The principal objective of our ongoing IRF project “Programs in the wild: Uncertainties, adaptability, and verification” is to provide a formal framework and tools for modelling and verifying the behaviour of systems characterised by a close interaction of a program with an unpredictable environment, like Cyber-Physical Systems (CPSs). In this talk we will discuss the …continue reading
Clemens Dubslaff: “Feature Causality”
Almost all practical software systems today are configurable. Huge configuration spaces, usually of size exponential in the number of configuration options or features, render their design, analysis, and explanation challenging tasks. In this talk, I will introduce the notion of “feature causality” to support explainability of configurable systems. Inspired by the seminal definition of actual …continue reading
Bas Luttik: About divergence-preserving branching bisimilarity
Jan Friso Groote: Another attempt to make BDDs more compact.
Quite some time ago I presented an approach to represent BDDs more compactly. The approach could be used to represent some formulas exponentially more compact than in ordinary BDDs. However, it was not possible to prove that this representation was never more than polynomially larger than BDDs. This approach turned out to be a particular …continue reading
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