Programme

The conference will take place on September 14-15, 2022 in Warschau.

Wednesday September 14.

9:00-9:05. Opening. Marieke Huisman.

9:05-10:00. Keynote (chair: Jan Friso Groote).
* Reinforcement Learning with Guarantees that Hold for Ever.
Sven Schewe.

10:30-12:00. Certification (chair: Bas Luttik).
* Formal Monotony Analysis of Neural Networks with Mixed Inputs: An asset for certification.
Guillaume Vidot, Melanie Ducoffe, Christophe Gabreau, Ileana Ober and Iulian Ober.
* Generating Interactive Validation Documents.
Fabian Vu, Christopher Happe and Michael Leuschel.
* Deductive Verification of Smart Contracts with Dafny.
Franck Cassez, Joanne Fuller and Horacio Mijail Anton Quiles.

14:00-16:00. Industrial use cases (chair: Sven Schewe).
* Towards Reusable Formal Models for Custom Real-time Operating Systems.
Julius Adelt, Julian Gebker and Paula Herber.
* Formal Verification of an Industrial UML-like Model using mCRL2.
Anna Stramaglia and Jeroen J.A. Keiren.
* Chemical Case Studies in KeYmaera X.
Rose Bohrer.
* Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining.
Jana Berger, Wiebke Lenze, Thomas Noll, Simon Schotten, Thorsten Büker, Mario Fietze and Bastian Kogel.

16:00-16:05. The best paper award and further announcements. Marieke Huisman

Thursday September 15.

9:00-10:00. Keynote (chair: Marieke Huisman).
* Supporting Railway Innovations with Formal Modelling and Verification.
Bas Luttik

10:30-12:00. Testing and monitoring (chair: Paula Herber).
* Test Suite Augmentation for Reconfigurable PLC Software in the Internet of Production.
Marco Grochowski, Marcus Völker and Stefan Kowalewski.
* Monitoring of Spatio-Temporal Properties with nonlinear SAT solvers.
André De Matos Pedro, Tomás Silva, Tiago Sequeira, João M. Lourenço, João Costa Seco and Carla Ferreira.
* Model-Based Testing of Internet of Things Protocols.
Xavier van Dommelen, Machiel van der Bijl and Andy Pimentel.

14:00-15:30. Methodology (chair: Wojciech Penczek).
* Formally Verifying Decompositions of Stochastic Specifications.
Anton Hampus and Mattias Nyberg.
* Verification of Behavior Trees using Linear Constrained Horn Clauses.
Thomas Henn, Marcus Völker, Stefan Kowalewski, Minh Trinh, Oliver Petrovic and Christian Brecher.
* A Multi-level Methodology for Behavioral Comparison of Software-Intensive Systems.
Dennis Hendriks, Arjan van der Meer and Wytse Oortwijn.