Tim Willemse: A Comparison of BDD-Based Parity Game Solvers (Joint work with Lisette Sanchez and Wieger Wesselink)
Parity games are two player games with omega-winning conditions, played on finite graphs. Such games play an important role in verification, satisfiability and synthesis. It is therefore important to identify algorithms that can efficiently deal with large games that arise from such applications. In this paper, we describe our experiments with BDD-based implementations of four …continue reading
Omar Alduhaiby: Learning Product Automata
Following a discussion with my colleague at University of Radboud Joshua Moerman on learning the product of independent automata, he pursued the subject of independence of outputs while I the independence of inputs. In this presentation I will summarise his recent paper titled ‘Learning Product Automata’ and how it relates to my work. I will …continue reading
Tatiana Shmeleva: Modeling Networks with Infinite Petri Nets
A composition and analysis technique is developed for investigation of infinite Petri nets with regular structure, introduced for modeling networks, clusters and computing grids, that also concerns cellular automata and biological systems. A case study of a square grid structure composition and analysis is presented. Parametric specification of Petri nets, parametric representation of infinite systems …continue reading
Maurice Laveaux: Verification in mCRL2 using multi-threaded algorithms: The term library.
Currently the mCRL2 toolset uses sequential algorithms exclusively. From these sequential algorithms the term rewriting algorithm often has the most prominent run-time cost. Developing a parallel term rewriting algorithm requires an efficient term library. This library facilitates the creation and destruction of terms. In this presentation I will present several challenges that I encountered while …continue reading
Hans Zantema: Making a MOOC
To make my lectures Automated Reasoning more accessible worldwide, I started developing a series of MOOCs (massive open online course). Professional facilities are provided by EIT Digital and Coursera. At the moment 21 lectures have been recorded, each covering around 10 minutes, by which the first MOOC on satisfiability is nearly finished. Roughly this MOOC …continue reading
Mahmoud Talebi: First-order Moment Closure Approximations for Middle-Sized Systems with Non-linear Rates
In this presentation I talk about the problem of approximating the behaviour of middle-sized population models involving non-linear rates. I describe a number of systems, each with a very different non-linear behaviour, and then show that the binomial and Poisson moment closure approximations have the potential to accurately represent the expected behaviour of these models. …continue reading
Wieger Wesselink: Counterexamples in the mCRL2 toolset
A long-standing problem in the mCRL2 toolset was the poor support for generating counterexamples of model checking properties. Over the course of the last year an effort has been made to finally tackle this problem. It is now possible to generate counterexamples and translate them back to the original model. The first applications of this …continue reading
Rodin Aarsen: Static Analysis on Legacy Software
Legacy software is a prominent bottleneck in modern industry: it is hard and costly to maintain, yet contains valuable knowledge not available elsewhere. Static analysis provides insight by extracting facts from existing code bases. In this talk, I will address complications and progress on my static analysis tooling in Rascal.
Pieter Hijma: Programming many-cores with the “Stepwise-refinement for performance” methodology
The main goal of this talk is to introduce my research to the FSA group and discuss possibilities and opportunities on how this research can be combined with model checking in general and with mCRL2 in particular in the context of the recently accepted TOP project AVVA (Accelerated Verification and Verified Acceleration). I will present …continue reading
Fei Yang: Two Problems on Context-free Processes and Pushdown Processes
In this talk, I will discuss two problems on examining in which cases context-free processes and pushdown processes are the same. In particular, we depart from the well-known case of language equivalence and instead look at processes using process theory and more fine-grained equivalences, such as branching bisimulation and contrasimulation. We identify two difficulties when …continue reading