OVERLAY 2025

Table of Contents

• PDF
  
• On the Verification of ML Systems and Models 3-12 PDF
  Greta Dolcetti, Vincenzo Arceri, Agostino Cortesi, Enea Zaffanella
• RNN Generalization to Omega-Regular Languages 15-21 PDF
  Charles Pert, Dalal Alrajeh, Alessandra Russo
• Passive Learning of Lattice Automata from Recurrent Neural Networks 23-32 PDF
  Jaouhar Slimi, Tristan Le Gall, Augustin Lemesle
• NAMOR: a New Agda Library for Modal Extended Sequents 33-40 PDF
  Riccardo Borsetto, Margherita Zorzi
• First-Order Linear Temporal Logic for Testing Distributed Protocols 41-48 PDF
  José João Ferreira, Nuno Policarpo, José Fragoso Santos, Alcino Cunha, Alessandro Gianola
• Automata Cascades for Model Checking 49-57 PDF
  Luca Geatti
• Fully Learnable Neural Reward Machines 59-66 PDF
  Hazem Dewidar, Elena Umili
• Towards Runtime Detection of Novel Traffic Situations 69-76 PDF
  Ishan Saxena, Dominik Grundt, Eike Möhlmann, Bernd Westphal
• Let the Music Flow Where the Modal Branches Lead 77-83 PDF
  Lorenzo Balboni, Federico Manzella, Guido Sciavicco
• Run-time verification of robot-assisted surgery using visual input 85-91 PDF
  Kristina Gogoladze, Romy van Jaarsveld, Natasha Alechina, Ronald de Jong, Yasmina Al Khalil, Gino Kuiper, Brian Logan, Jelle P. Ruurda
• Leveraging LLMs for Formal Software Requirements: Challenges and Prospects 95-105 PDF
  Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan
• A Proposal For Handling Query Ambiguity For Process Mining Tasks 107-115 PDF
  Lucas Fortunato Das Neves, Chrysoula Zerva, Alessandro Gianola
• Learning to Coordinate without Communication under Incomplete Information 119-126 PDF
  Shenghui Chen, Shufang Zhu, Giuseppe De Giacomo, Ufuk Topcu
• Strategic Reasoning over Golog Programs in the Nondeterministic Situation Calculus -- Extended Abstract 127-132 PDF
  Giuseppe De Giacomo, Yves Lespérance, Matteo Mancanelli
• Circuit Complexity Meets Discrete Ordinary Differential Equations: An Overview 135-142 PDF
  Melissa Antonelli, Arnaud Durand, Juha Kontinen
• From Applicative Programming to Verification-based Knowledge: A Curry-Howard-Lambek Reading 143-152 PDF
  Cosimo Perini Brogi
• Attack logics, not outputs: Towards efficient robustification of deep neural networks by falsifying concept-based properties 153-165 PDF
  Raik Dankworth, Gesina Schwalbe
• RLRom: Monitoring and Training Reinforcement Learning Agents using Signal Temporal Logic 167-172 PDF
  Ana María Gómez-Ruiz, Alexandre Donzé, Thao Dang
• A Proof System with Causal Labels (Part I): checking Individual Fairness and Intersectionality 173-179 PDF
  Leonardo Ceragioli, Giuseppe Primiero
• A Proof System with Causal Labels (Part II): checking Counterfactual Fairness 181-187 PDF
  Leonardo Ceragioli, Giuseppe Primiero
• False Positives in Robustness Checking of Neural Networks 189-197 PDF
  Mohammad Afzal, Ashutosh Gupta, R. Venkatesh, S. Akshay
• Compliance Checking for Public Administration Processes using Retrieval-Augmented Generation in LLMs: Novel Directions and Challenges 199-208 PDF
  Alessandro Gianola, Chrysoula Zerva
• Reasoning on Privacy Policies 209-218 PDF
  Yilian Huang, Cosimo Perini Brogi, Rocco De Nicola
• Extracting Weighted Finite Automata from RNNs via iterative partitioning and spectral learning 219-225 PDF
  Sandamali Yashodhara Wickramasinghe, Jacob M. Howe, Laure Daviaud