Wednesday 20 September
9:00 - 10:00 | Invited Talk: Joost-Pieter Katoen (joint with CONFEST) | Verification Conquers Fault Tree Analysis |
10:00 - 10:20 | Coffee break | |
10:20 - 12:20 | Session 1: Verification (chair: Maurice ter Beek) | |
10:20 - 10:50 | Neelanjana Pal, Diego Manzanas Lopez and Taylor T Johnson | Robustness Verification of Deep Neural Networks using Star-Based Reachability Analysis with Variable Length Time Series Input |
10:50 - 11:20 | Huan Sun, Ziyu Mao, Jingyi Wang, Ziyan Zhao and Wenhai Wang | Applying Rely-guarantee Reasoning on Concurrent Memory Management and Mailbox in μc/OS-II: A Case Study |
11:20 - 11:50 | Kim Guldstrand Larsen, Axel Legay and Danny Bøgsted Poulsen | Refinement of Systems with an Attacker Focus |
11:50 - 12:20 | Lukas Dust, Rong Gu, Cristina Seceleanu, Mikael Ekström and Saad Mubeen | Pattern-Based Verification of ROS 2 Nodes using UPPAAL |
15:00 - 17:00 | Social event: Boat trip on Scheldt river | |
19:30 | Conference dinner | |
Thursday 21 September
9:00 - 10:00 | Invited Talk: Jaco van de Pol (joint with CONFEST) | Encoding Planning and Games in SAT and QBF |
10:00 - 10:20 | Coffee break | |
10:20 - 12:20 | Session 2: Model Checking and Temporal Logics (chair: Alessandro Fantechi) | |
10:20 - 10:50 | Aziz Sfar, David Carral, Dina Irofti and Madalina Croitoru | Testing Logical Diagrams in power plants: a tale of LTL model checking |
10:50 - 11:20 | Francisco Durán, Nicolás Pozas, Carlos Ramírez and Camilo Rocha | Statistical Model Checking for P |
11:20 - 11:50 | Chris Johannsen, Brian Kempa, Phillip Jones, Kristin Rozier and Tichakorn Wongpiromsarn | Impossible Made Possible: Encoding Intractable Specifications via Implied Domain Constraints |
11:50 - 12:20 | Reza Soltani, Matthias Volk, Leonardo Diamonte, Milan Lopuhaä-Zwakenberg and Mariëlle Stoelinga | Optimal spare management via statistical model checking: A case study in research reactors |
12:20 - 13:45 | Lunch | |
13:45 - 14:45 | Invited Talk: Anna Slobodova (chair: Laura Titolo) | Combining automation with hands-on reasoning |
14:45 - 15:45 | Session 3: Testing (chair: Hubert Garavel) | |
14:45 - 15:15 | John Hatcliff, Jason Belt, Fnu Robby, Jacob Legg, Danielle Stewart and Todd Carpenter | Automated Property-based Testing from AADL Component Contracts |
15:15 - 15:45 | Bence Graics, Vince Molnár and Istvan Majzik | |
15:45 - 16:00 | Coffee break | |
16:00 - 17:00 | Invited Talk: Dave Parker (joint with CONFEST) | Multi-Agent Verification and Control with Probabilistic Model Checking |
17:30 - 20:00 | Soccer Match | |
Friday 22 September
9:00 - 10:00 | Invited Talk: Ahmed Bouajjani (joint with CONFEST) | On the verification of concurrent programs under weak consistency models |
10:00 - 10:20 | Coffee break | |
10:20 - 12:20 | Session 4: Applications (chair: Cristina Seceleanu) | |
10:20 - 10:50 | Davide Basile, Franco Mazzanti and Alessio Ferrari | Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect |
10:50 - 11:20 | Dimitri Belli, Alessandro Fantechi, Stefania Gnesi, Laura Masullo, Franco Mazzanti, Lisa Quadrini, Daniele Trentini and Carlo Vaghi | The 4SECURail case study on rigorous standard interface specifications |
11:20 - 11:50 | Djurre van der Wal, Marcus Gerhold and Marielle Stoelinga | [Best paper] Conformance in the Railway Industry: Single-Input-Change Testing a EULYNX Controller |
11:50 - 12:20 | Imran Riaz Hasrat, Jiřı Srba, Peter Gjøl Jensen and Kim Guldstrand Larsen | Modelling of Hot Water Buffer Tank and Mixing Loop for an Intelligent Heat Pump Control |