| Program |
| Day 1 : November 19 |
| 09H00 - 09H30 | Welcome & Registration |
| 09H30 - 10H00 | VECoS 2026 Opening Session |
| 10H00 - 12H30 | Session 1: Formal methods |
| 10H00 - 10H30 | Demis Ballis, Linda Brodo, Moreno Falaschi and Carlos Olarte. Formal Analysis of Reaction Systems Using Maude Strategies |
| 10H30 - 11H00 | Valentin Bergeron and Karolina Gorna. From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware |
| 11H00 - 11H30 | Coffee Break |
| 11H30 - 12H00 | Khadija Khlass, Belgacem Ben Hedia and Boutheina Bannour. Behavioral Preservation and the Cost of Granularity in Verifying Re-Clustered Critical Real-Time Software Deployments |
| 12H00 - 12H30 | Ocan Sankur, Reiya Noguchi, Thierry Jéron and David Mentré. ReqKit: A Real-Time Requirement Analysis Tool Kit |
| 12H30 - 14H00 | Lunch |
| 14H00 - 15H00 | Invited Talk (Pr Sandjai Bhulai) : Performance evaluation in the age of learning and search |
| 15H00 - 18H00 | Session 2: Safety verification |
| 15H00 - 15H30 | Oumaima Barhoumi, Mohamed H Zaki and Sofiène Tahar. Formally Verified Higher-Order Barrier Certificates for Vehicle Platooning |
| 15H30 - 16H00 | Coffee Break |
| 16H00 - 16H30 | Mohamed Achraf Touam, Rabéa Ameur-Boulifa and Patricia Guitton-Ouhamou. A Tool-Supported Methodology for Early Requirement Verification: From Natural-Language Requirements to Verifiable SCADE Models |
| 16H30 - 17H00 | Sami Mahfoudhi, Hassen M. Ouakad and Kamel Barkaoui. Experience-Driven RAG for VLM-Based Fixed-Wing UAV Obstacle Avoidance |
| 19H- | Social Event - Scientific discussions - Gala dinner |
| Day 2 : November 20 |
| 09H00 - 10H00 | Invited Talk (Pr Karsten Wolf) : A fresh look into modular state spaces for Petri nets |
| 10H00 - 12H30 | Session 3 : Petri net formalism |
| 10H00 - 10H30 | Kais Klai, Mohamed Taha Bennani, Jaime Arias and Hanen Ochi. Optimizing Petri Net Transition Coverage for Test Generation Using Linear Programming and Symbolic Observation Graphs |
| 10H30 - 11H00 | Coffee Break |
| 11H00 - 11H30 | Mouna Gaouar, Rabah Ammour, Isabel Demongodin and Olivier H. Roux. Semi Synchronized and Time Synchronized Petri Nets with Outputs: decidability properties and reachability marking spaces |
| 11H30 - 12H00 | Clément Lecomte and Patrice Bonhomme. Formal Shields for IDS Resilience: An IP-TPN/DRL Digital Twin for Measuring Residual Exfiltration Capacity |
| 12H00 - 12H30 | Eya Teyeb, Pierre Delisle, Luiz Angelo Steffenel and Leonardo Brenner. Constant Batch-Level Speed Limits in Controlled Triangular Batches Petri Nets |
| 12H30 - 14H00 | Lunch |
| 14H00 - 17H00 | Session 4 : Architecture analysis |
| 14H00 - 14H30 | Morten Clausen and Pınar Tözün. Analytical Framework for Algorithms on Collaborative Heterogeneous Architectures |
| 14H30 - 15H00 | Hai-Dang Vu, Mihail Asavoae and Oumaima Matoussi. From Proprietary Architecture Descriptions to Formal ISA Semantics |
| 15H00 - 15H30 | Coffee Break |
| 15H30 - 16H00 | Ranim Ghodhbani, Rim Saddem-Yagoubi and Julie Beugin. Requirement-Driven Evolution of ETCS Moving Block Architectures: Extended Analysis and Tool Support |
| 16H00 - 16H30 | Kahina Ferhi, Assia Outamazirt, Djamil Aissani, Kamel Barkaoui and Karima Adel-Aissanou. CAS-Greedy: A Deterministic Carbon-Aware Scheduler for the Cloud--Edge Continuum Based on a Five-Term Multi-Objective Cost Function |
| 16H30 - 17H00 | Closing session (infos about VECoS 2027) |
