Starting on Juli 1, 2021 Tim Willemse took over the role of cluster leader of FSA from Jan Friso Groote who has been leader for more than 20 years.
Author: Jan Friso Groote
Leo van Schooten graduated
On May 10, 2021 Leo van Schooten successfully defended his thesis on translating a DSL in use at Philips to specify and control X-ray capabilities to the language Dezyne, allowing for a less complex software generation process, and enabling the possibility to automatically verify correctness properties.
Proceedings TACAS 2021 are online
The proceedings of TACAS 2021 are online (LNCS 12651 and LNCS 12652). Editors are J.F. Groote and K.G. Larsen. They are open access.
Big software project MERITS finished
The NWO Big Software project MERITS is finished. It investigated whether refactoring of legacy software is possible by automatic learning. The conclusion is that this is a bridge too far, but learning techniques are an effective means to get structural insight in software that is otherwise hard to obtain. Read the the full report.
Paper accepted at Concur2020
A paper containing a near-linear time algorithm for weak bisimilarity for Markov chains, by Jansen, Groote, Timmers and Yang has been accepted at Concur 2020. The paper provides an average time O(m log^4 n) algorithm, which is a substantial improvement over the best O(m n) algorithm hitherto known.
Jan Martens new PhD student
At Februari 1, 2020, Jan Martens joined us as a new PhD student in the AVVA project. Jan will direct his attention to the question how many core architectures, such as GPU’s, can improve the capabilities to analyse behavioural models.
Paper accepted at Express
The paper Distribution of Behaviour into Parallel Communicating Subsystems by Omar Alduhaiby and Jan Friso Groote has been accepted for Express 2019.
Paper on the analysis of hyper torus communication grids.
The paper “Verification of Hypertorus Communication Grids by Infinite Petri Nets and Process Algebra” by Zaitsev, Shmeleva and Groote has been published in IEEE/CAA Automata Sinica. The paper explains how communication grids in the form of hyper toruses can be verified using both Petri Nets and mCRL2 in an efficient manner.
Ferry Timmers started in the Arrowheads project.
On April 15 Ferry Timmers started in the Arrowheads project together with ASML. The goal of this project is to show that newly developed control software for wafer scanners can completely be verified before the software is tested and deployed.
Paper on hypertorus grids accepted
The paper “Verification of Hypertorus Communication Grids by Infinite Petri Nets and Process Algebra” by Zaitsev, Shmeleva and Groote has been accepted for the IEEE/CAA journal of Automatica Sinica.