## Alexander Fedotov: McMillan’s algorithm for SAT-based unbounded model checking.

In this talk, I will discuss McMillan’s algorithm for fully SAT-based unbounded symbolic model checking. The method is based on computing Craig interpolants. In terms of performance, the algorithm is substantially more efficient than BDD-based model checking. I will also explain how we modify McMillan’s algorithm to analyze the backward reachability of initial states from *…continue reading*

## Flip van Spaendonck: Understanding std::memory_order in C++11 using MCA semantics

C++11 introduced many tools to write safe multi threaded code. One of those tools are the std::memory_orders, which specify how memory accesses, including regular, non-atomic memory accesses, are to be ordered around atomic operations. Understanding these memory orders can be quite a complex situation, specifically when different memory orders are combined. We will try to make *…continue reading*

## Geert van Ieperen: Visualisation of large Labelled Transition Systems

A formal model describes the behaviour of a program, protocol or other system. The properties of this model can be verified, such that we can prove these properties with absolute certainty. Visualising the state space of a formal model is an important tool for their development. This thesis focuses on visualising such a state space *…continue reading*

## Anna Stramaglia: Deadlock in packet switching networks

A deadlock in a packet switching network is a state in which one or more messages have not yet reached their target, yet cannot progress any further. We formalize three different notions of deadlock in the context of packet switching networks, to which we refer as global, local and weak deadlock. We establish the precise *…continue reading*

## Muhammad Osama: SAT Solving with GPU Accelerated Inprocessing

Since 2013, the leading SAT solvers in the SAT competition all use inprocessing, which unlike preprocessing, interleaves search with simplifications. However, applying inprocessing frequently can still be a bottle neck, i.e., for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As memory is a scarce *…continue reading*

## Rick Erkens: A Set Automaton to Locate All Pattern Matches in a Term

Term pattern matching is the problem of finding all pattern matches in a subject term, given a set of patterns. It is a fundamental algorithmic problem in for instance automated theorem proving and term rewriting. We present a set automaton solution for the term pattern matching problem that is based on match set derivatives where *…continue reading*

## Bas Luttik: Equationally axiomatising parallel composition

I will overview some results pertaining to the (equational) axiomatisation of interleaving parallel composition.

## Jan Friso Groote: Partition refinement algorithms for strong bisimulation are Omega(n log n)

A question haunting me for a while is whether the O(m log n) algorithm for strong bisimulation is optimal. We found a family of graphs that shows that any reasonable partition refinement algorithm is necessarily Omega(n log n), n being the number of states, steps to calculate strong bisimulation. This appeared to answer the question. *…continue reading*

## Hans Zantema: Complexity of Simon’s problem in classical sense

Simon’s problem is a standard example of a problem that is exponential in classical sense, while it admits a linear solution in quantum computing. It is about a function f for which it is given that a unique non-zero vector s exists for which f(x) = f(x xor s) for all x. The goal is to find s. The *…continue reading*

## Jan Martens: Solving bisimilarity and the relational coarsest partition problem in sub-linear parallel time seems hard

It is known that deciding bisimilarity is a P-complete problem. This means it is thought of as a problem that is inherently sequential and hard to solve in parallel. Despite this fact efforts have been made to construct increasingly efficient parallel algorithms. In a previous colloquium I presented a parallel algorithm that decides bisimilarity in *…continue reading*