The PaVeS project is represented at ATVA’20 with two contributions: Peregrine 2.0: Explaining Correctness of Population Protocols through Stage Graphs by Javier Esparza, Martin Helfrich, Stefan Jaax, and Philipp J. Meyer Complexity of Verification and Synthesis of Threshold Automata by A. R. Balasubramanian, Javier Esparza and Marijana Lazić
As mentioned in the previous news the PaVeS group contributed successfully to LICS’20. Another contribution of a PaVeS member is the paper “The Complexity of Reachability in Affine Vector Addition Systems with States” of Mikhail Raskin and Michael Blondin.
There are good news to be announced for the 1st quarter of 2020: The paper “An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata” by Salomon Sickert and Javier Esparza was accepted at LICS’20. The paper “Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling” Read more…
Philip Offtermatt successfully defended his Master’s thesis “Approaching Safety for Parameterized Systems via View Abstraction”. Furthermore, we want to announce the first PaVeS Christmas workshop. It is planned for the 16th December.
Michael Luttenberger, Philipp Meyer and Salomon Sickert-Zehnter published their article “Practical synthesis of reactive systems from LTL specifications via parity games” in Acta Informatica.
This month two PhD students join the PaVeS team. Martin Helfrich was already party of PaVeS as a student assistant. Now he started his PhD. Furthermore, we welcome A. R. Balasubramanian as our newest team member!
Today, as for the last several Tuesdays, the chairs i2 and i7 celebrated a joint coffee break. This time Chana took this picture of the cake present which we are proud to present!
Javier Esparza attended the 13th Alpine Verification Meeting from September 9th – September 11th and gave an invited talk at September 10th with the title “Population protocols: A Case Study in Parameterized Verification of Liveness Properties of Probabilistic Distributed Algorithms”.
As in the year before , Strix won this year’s SYNTCOMP competition in the TLSF/LTL Synthesis Track. Furthermore, the techniques used in Strix will be described in detail in an article which is scheduled to be published in Acta Informatica.
The paper Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries of Marijana Lazic, Nathalie Bertrand, Igor Konnov and Josef Widder was accepted at CONCUR’19.