Proceedings
Formal Methods for AI Proceedings of the 7th International Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis Bologna (Italy), October 26, 2025 https://overlay.uniud.it/workshop/2025 Copyright © 2025 for the individual papers by the papers’ authors. Copyright © 2025 for the volume as a collection by its editors. This volume and its papers are published under the
Creative Commons License Attribution 4.0 International (CC BY 4.0). Workshop organization
Angelo Montanari AndreA Orlandini Nicola Saccomanno Stefano Tonetta
Raul Barbosa Saddek Bensalem Alberto Bombardelli Laura Bozzelli Davide Bresolin Alessandro Burigana Görschwin Fey Mirco Giacobbe Alessandro Gianola Nicola Gigante Laura Giordano Martin Leucker Federico Mari Andrea Micheli Sergio Mover Carla Piazza Ingo Pill Michel Reniers Sabina Rossi Sasha Rubin Cesar Sanchez Enrico Tronci Sarah Winkler Matteo Zavatteri
Martin Zimmermann
Nicola Gigante
University of Udine, Italy National Research Council of Italy, Italy University of Udine, Italy Fondazione Bruno Kessler, Italy University of Coimbra, Portugal VERIMAG, France Fondazione Bruno Kessler, Italy Federico II University of Naples, Italy University of Padua, Italy Free University of Bozen-Bolzano, Italy Hamburg University of Technology, Germany University of Birmingham, United Kingdom INESC-ID/Instituto Superior Técnico, Universidade de Lisboa, Portugal Free University of Bozen-Bolzano, Italy University of Eastern Piedmont, Italy University of Luebeck, Germany University of Rome Foro Italico, Italy Fondazione Bruno Kessler, Italy Ecole Polytechnique, France University of Udine, Italy Graz University of Technology, Austria Eindhoven University of Technology, Netherlands Ca’ Foscari University of Venice, Italy The University of Sydney, Australia IMDEA Software Institute, Spain Sapienza University of Rome, Italy Free University of Bozen-Bolzano, Italy University of Padova, Italy Aalborg University, Denmark
Free University of Bozen-Bolzano, Italy
Greta Dolcetti, Vincenzo Arceri, Agostino Cortesi, Enea Zafanella
Charles Pert, Dalal Alrajeh, Alessandra Russo
Jaouhar Slimi, Tristan Le Gall, Augustin Lemesle
Riccardo Borsetto, Margherita Zorzi
José João Ferreira, Nuno Policarpo, José Fragoso Santos, Alcino Cunha, Alessandro Gianola
Luca Geatti
Hazem Dewidar, Elena Umili
Ishan Saxena, Dominik Grundt, Eike Möhlmann, Bernd Westphal
Lorenzo Balboni, Federico Manzella, Guido Sciavicco
Leveraging LLMs for Formal Software Requirements: Challenges and Prospects Arshad Beg, Diarmuid O’Donoghue, Rosemary Monahan
Lucas Fortunato Das Neves, Chrysoula Zerva, Alessandro Gianola
Learning to Coordinate without Communication under Incomplete Information Shenghui Chen, Shufang Zhu, Giuseppe De Giacomo, Ufuk Topcu Strategic Reasoning over Golog Programs in the Nondeterministic Situation Calculus – Extended
Giuseppe De Giacomo, Yves Lespérance, Matteo Mancanelli
Circuit Complexity Meets Discrete Ordinary Diferential Equations: An Overview Melissa Antonelli, Arnaud Durand, Juha Kontinen From Applicative Programming to Verification-based Knowledge: A Curry-Howard-Lambek Reading Cosimo Perini Brogi Attack logics, not outputs: Towards eficient robustification of deep neural networks by falsifying concept-based properties Raik Dankworth, Gesina Schwalbe RLRom: Monitoring and Training Reinforcement Learning Agents using Signal Temporal Logic Ana María Gómez-Ruiz, Alexandre Donzé, Thao Dang A Proof System with Causal Labels (Part I): checking Individual Fairness and Intersectionality Leonardo Ceragioli, Giuseppe Primiero A Proof System with Causal Labels (Part II): checking Counterfactual Fairness Leonardo Ceragioli, Giuseppe Primiero
Mohammad Afzal, Ashutosh Gupta, R. Venkatesh, S. Akshay Compliance Checking for Public Administration Processes using Retrieval-Augmented Generation in LLMs: Novel Directions and Challenges Alessandro Gianola, Chrysoula Zerva
Yilian Huang, Cosimo Perini Brogi, Rocco De Nicola Extracting Weighted Finite Automata from RNNs via iterative partitioning and spectral learning Sandamali Yashodhara Wickramasinghe, Jacob M. Howe, Laure Daviaud The use of Artificial Intelligence (AI) within the context of safety-critical systems has been experiencing continuous growth for a number of years now. On top of that, the research community is currently aiming to integrate sub-symbolic approaches with symbolic ones to foster their usage in critical scenarios such as, for example, safety-critical systems. These applications call for the adoption of Formal Methods (FM) techniques for the design, verification and synthesis of reliable and robust systems. The intersection between the AI and the FM communities is therefore more and more important.
OVERLAY 2025 was the 7th edition of the International Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis. Supported by the OVERLAY group (https://overlay.uniud.it), its primary objective is to establish and sustain a long lasting scientific platform dedicated to topics in the intersection of AI and FM.
This year’s edition (https://overlay.uniud.it/workshop/2025/) took place on October 26, 2025 at the Engineering School of the University of Bologna, Italy, and was part of the 28th edition of the European Conference on Artificial Intelligence held in Bologna from the 25th to the 30th of October 2025.
The review process involved 25 PC members (plus 5 additional sub-reviewers) whose afiliations came from 10 diferent countries: Australia (1), Austria (1), Denmark (1), France (2), Germany (2), Italy (17), Netherlands (1), Portugal (2), Spain (1), United Kingdom (1). Eventually, 19 papers and 10 work-in-progress papers were accepted for presentation out of a total of 34 submissions that involved 90 authors whose afiliations came from 14 diferent countries: Canada, Denmark, Finland, France, Germany, India, Ireland, Italy (42), Netherlands, Norway, Portugal, Switzerland, United Kingdom, and USA. Of the accepted papers, 5 were not included in these proceedings by request of the authors.
Six sessions organized the presentations of the accepted papers: • Session 1: Verification of learning-based and multi-agent systems, chaired by Stefano Tonetta (Fondazione
Bruno Kessler, Italy); • Session 2: Automata, formal languages and logic, chaired by Angelo Montanari (University of Udine, Italy); • Session 3: Applications of formal verification and AI, chaired by Nicola Saccomanno (University of Udine,
Italy); • Session 4: LLMs and Neurosymbolic AI for knowledge acquisition, chaired by Andrea Orlandin (CNR, Italy); • Session 5: Games and reasoning, chaired by Andrea Orlandini (CNR, Italy); • Session 6: Spotlight presentations of Work in Progress, chaired by Nicola Saccomanno (University of Udine,
Italy).
In addition a Poster session was organized with 10 extended abstracts, accepted as work in progress. In general, the accepted contributions exemplify seamless integration between artificial intelligence and formal methods.
OVERLAY 2025 witnessed a vibrant participation of around 80 attendees, fostering discussions among researchers bridging the realms of AI and FM. The contributions collected in these proceedings also prove the outstanding quality of the submissions received.
A huge thank you goes to Nicola Gigante at the Free University of Bolzano who kept the OVERLAY website always up to date and contributed in the formatting of these proceedings.
Finally, we extend our sincere gratitude to all authors and participants, and wish to reiterate once more that OVERLAY represents far more than a traditional workshop.
The chairs, Angelo Montanari, University of Udine, Italy AndreA Orlandini, CNR, Italy Nicola Saccomanno, University of Udine, Italy Stefano Tonetta, Fondazione Bruno Kessler, Italy.