## Jeroen Keiren: Itβs all a game: Bisimulation and Apartness

Strong apartness has been proposed as a relation for distinguishing states in a labelled transition system. Prior work has shown that there is a clear connection between Hennessy-Milner logic, strong bisimilarity and strong apartness. In this talk, I discuss the connection between apartness and bisimulation games. In particular, I show that in a bisimulation game, *…continue reading*

## Edward Liem: Towards Optimizing Feature Cause Computations

Configurable systems enables customization of features to alter system functionalities. However, feature modifications have the potential to impact security, safety or usability of the configured system. In many cases, configuration spaces tend to be exponential w.r.t. the number of features, hampering detection and explanation of behaviors of interest. Recent works have introduced the notion of *…continue reading*

## Anton Wijs: Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking

The need for massively parallel algorithms, suitable to exploit the computational power of hardware such as graphics processing units, is ever increasing. We propose a new explicit-state model checking algorithm for the on-the-fly verification of Linear-Time Temporal Logic (LTL) formulae that is aimed at running on such devices. We prove its correctness and termination guarantee, *…continue reading*

## Anna Stramaglia: Efficient Evidence Extraction from PBESs

Model checking is a technique to automatically assess the quality of software and hardware systems. Given a system specification and a requirement, a model checker returns the answer to the model checking problem, true or false. In case the result is not as expected the model checker desireably provides evidence to explain why the answer *…continue reading*

## Clemens Dubslaff: Template Decision Diagrams for Meta Control and Explainability

Decision tree classifiers (DTs) provide an effective machine-learning model, well-known for its intuitive interpretability. However, they still miss opportunities well-established in software engineering that could further improve their explainability: separation of concerns, encapsulation, and reuse of behaviors. To enable these concepts, we recently introduced templates in decision diagrams (DDs) as an extension of multi-valued DDs. *…continue reading*

## Thomas Neele: A new Operational and Axiomatic semantics for AuDaLa

The Autonomous Data Language (AuDaLa) is a recently introduced programming language and is supported by an operational semantics. I this talk I will present a new operational semantics for AuDaLa with relaxed memory consistency and incoherent memory, with the goal of allowing more compiler optimisations. Under certain conditions, the new semantics are equivalent to the *…continue reading*

## Herman Geuvers: alpha-equivalence

The notion of πΌ-equivalence between π-terms is used to identify terms that are considered equal modulo renaming bound variables. Using De Bruijn indices we can give a unique representation for closed π-terms modulo πΌ-equivalence. Equating terms that have the same De Bruijn representation falls short when comparing subterms occurring within a larger context: it may *…continue reading*

## Tom Franken: Proving a Parallel Sorting Algorithm in AuDaLa

In this presentation, I will recap the concepts of AuDaLa and give the design of a parallel sorting algorithm, Insertion Sort, which requires the use of write-write data races. I will prove this algorithm correct, during which I will discuss finding data races in AuDaLa, creating contracts for AuDaLa steps and basic lemmas to help *…continue reading*

## Flip van Spaendonck: Modelling Object-Oriented Code

In my previous colloquium talk, I gave a brief overview of how we automatically transform object-oriented C++ code into labeled transition systems using our novel State-Space Transformation & Generation tool (SSTraGen). In this talk, we skip the transformation step, and instead, take a more detailed look at the precise semantics used for capturing the various *…continue reading*

## Tim Willemse: On the minimisation of transition systems

There is a wealth of equivalence relations on labelled transition systems; see, e.g., Van Glabbeek’s linear-time branching-time spectrum. Some of these equivalences have found their way in tool sets such as mCRL2, where they are used either to compare two transition systems, or to reduce the size of a transition system. The latter is often *…continue reading*