Programming Languages and Systems 35th European Symposium on Programming, ESOP 2026, Held as Part of the International Joint… (Robbert Krebbers) (z-library.sk, 1lib.sk, z-lib.sk)

K rebbers (Ed.) Program m ing Languages and System s 35th European Symposium on Programming, ESOP 2026 Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026 Turin, Italy, April 11–16, 2026, Proceedings, Part I Programming Languages and SystemsLN CS 1 65 01 AR Co SS Robbert Krebbers (Ed.)

Lecture Notes in Computer Science 16501 Founding Editors Gerhard Goos Juris Hartmanis Editorial Board Members Elisa Bertino , USA Wen Gao, China Bernhard Steffen , Germany Moti Yung , USA Advanced Research in Computing and Software Science Subline of Lecture Notes in Computer Science Subline Series Editors Giorgio Ausiello, University of Rome ‘La Sapienza’, Italy Vladimiro Sassone, University of Southampton, UK Subline Advisory Board Susanne Albers, TU Munich, Germany Benjamin C. Pierce, University of Pennsylvania, USA Bernhard Steffen , University of Dortmund, Germany Deng Xiaotie, Peking University, Beijing, China Jeannette M. Wing, Microsoft Research, Redmond, WA, USA

More information about this series at https://link.springer.com/bookseries/558

Robbert Krebbers Editor Programming Languages and Systems 35th European Symposium on Programming, ESOP 2026 Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026 Turin, Italy, April 11–16, 2026 Proceedings, Part I

Editor Robbert Krebbers Radboud University Nijmegen Nijmegen, The Netherlands ISSN 0302-9743 ISSN 1611-3349 (electronic) Lecture Notes in Computer Science ISBN 978-3-032-22719-5 ISBN 978-3-032-22720-1 (eBook) https://doi.org/10.1007/978-3-032-22720-1 © The Editor(s) (if applicable) and The Author(s) 2026. This book is an open access publication. Open Access This book is licensed under the terms of the Creative Commons Attribution- NonCommercial-NoDerivatives 4.0 International License (http://creativecommons.org/licenses/by-nc-nd/ 4.0/), which permits any noncommercial use, sharing, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if you modified the licensed material. You do not have permission under this license to share adapted material derived from this book or parts of it. The images or other third party material in this book are included in the book’s Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book’s Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. Thiswork is subject to copyright. All commercial rights are reserved by the author(s), whether thewhole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction onmicrofilms or in any other physical way, and transmission or information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed. Regarding these commercial rights a non-exclusive license has been granted to the publisher. The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. The publisher, the authors and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors give a warranty, expressed or implied, with respect to the material contained herein or for any errors or omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in published maps and institutional affiliations. Please refer to the chapters to see the exact Creative Commons Attribution licenses that apply in each case. This Springer imprint is published by the registered company Springer Nature Switzerland AG The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland If disposing of this product, please recycle the paper.

ETAPS Foreword Welcome to the 29th edition of ETAPS, which took place as an on-site event in Turin, Italy during April 11–16, 2026! ETAPS 2026 was the 29th instance of the International Joint Conferences on Theory and Practice of Software (ETAPS). ETAPS is an annual federated conference established in 1998, and consists of four main conferences: ESOP, FASE, FoSSaCS, and TACAS. Each conference has its own Program Committee (PC) and its own Steering Committee (SC). The ETAPS main conferences cover various aspects of software systems, ranging from theoretical computer science to foundations of programming languages, tools and algorithms for system analysis, and formal approaches to software engineering. Organiz- ing these conferences in a coherent, highly synchronized conference programme enables researchers to participate in an exciting event, having the possibility to meet many col- leagues working in different directions in the field, and to easily attend talks of different conferences. In addition to its four main conferences, ETAPS 2026 also hosted fifteen satellite workshops and two colocated events, which together further attracted many researchers from all over the globe. ETAPS 2026 received 456 submissions in total, 138 ofwhichwere accepted, yielding an overall acceptance rate of 30%. Out of the 138 accepted papers, 16 papers were selected as ETAPS distinguished papers. I thank all the authors of submitted papers for their interest in ETAPS, all the reviewers for their reviewing efforts, the PCmembers for their contributions, and in particular the PC (co-)chairs for their hardwork in running this entire intensive process in a constructive, objective and timely manner. I congratulate all authors of the ETAPS 2026 accepted papers! ETAPS 2026 featured the unifying invited keynotes by – Monika Henzinger (Institute of Science and Technology Austria, Austria), delivering a talk about “Guarding Privacy Over Time: Challenges and Solutions in Continuous Data Observation”, – Einar Broch Johnsen (University of Oslo, Norway), discussing “Formal Methods Meet Digital Twins: Challenges and Opportunities”. ETAPS 2026 hosted the invited keynote speakers – Christel Baier (Technische Universität Dresden, Germany) for FoSSaCS, presenting “Verification of Infinite-horizon Properties of Dynamic Bayesian Networks”, – Guy Van den Broeck (University of California, Los Angeles, USA) for TACAS, introducing “Symbolic Reasoning in the Age of Large Language Models”. The ETAPS 2026 invited tutorials were provided by – Mieke Massink (CNR-ISTI Pisa, Italy) on “Model Checking in Space with Applica- tions to Medical Image Analysis”, – Leonardo de Moura (Amazon Web Services, USA) surveying “The Lean Program- ming Language and Theorem Prover”.

vi ETAPS Foreword The ETAPS 2026 programme also featured a lively Ask-Me-Anything session, inter- active tool demos, a Diversity, Equity, and Inclusion session, SV-Comp and Test-Comp community building events, and the ETAPS industry day. The goal of the ETAPS indus- try day is to bring industrial practitioners into the heart of the research community and to catalyze the interaction between industry and academia. The ETAPS 2026 indus- try day was organized by Giorgio Audrito (University of Turin, Italy), Sean Kauffman (Queen’s University, Kingston, Canada), and Nikolai Kosmatov (Thales Research and Technology, Palaiseau, France). ETAPS 2026 was organized by the Department of Computer Science of the Uni- versity of Turin, which is the center for coordinating research, teaching, dissemination and technological transfer in computer science in Turin, Italy. The department covers bothmethodological and application oriented aspects of computer science, and performs research in several interdisciplinary areas. This is reflected in the collaborations with other research centers and companies in many scientific areas and in its participation in national, European and international projects. ETAPS 2026 was further supported by the following associations and societies: ETAPS e. V. (the ETAPS Association), EATCS (European Association for Theoretical Computer Science), EAPLS (European Association for Programming Languages and Systems), and EASST (European Association of Software Science and Technology). The ETAPS Steering Committee consists of an Executive Board, and representatives of the individual ETAPS conferences, as well as representatives of EATCS, EAPLS, and EASST. The Executive Board consists of Laura Kovács (TU Wien, chair), Andrzej Wa̧sowski (IT University of Copenhagen, vice-chair), Thomas Noll (RWTH Aachen, treasurer), Arnd Hartmanns (University of Twente, artifact evaluation coordinator), Bar- bara König (University of Duisburg-Essen, proceedings coordination), Caterina Urban (Inria, PhD activities), Elizabeth Polgreen (University of Edinburgh, social media), Jan Kofroň (Charles University Prague, organisational support, website), Jan Křetínský (Masaryk University Brno and TU Munich, diversity & inclusion), and Marieke Huis- man (University of Twente, blog, awards). Further members of the ETAPS Steering Committee committee are: Robbert Krebbers (Radboud University Nijmegen), Azalea Raad (Imperial College London), Luı́s Caires (Tecnico ULisboa), Elvira Albert (Univer- sidad Complutense de Madrid), Corina Păsăreanu (Carnegie Mellon University), Erika Ábrahám (RWTH Aachen), Marsha Chechik (University of Toronto), Marie-Christine Jakobs (LMU Munich), Nathalie Bertrand (Inria Rennes), Stefan Milius (Friedrich- Alexander Universität Erlangen-Nürnberg), Alexandra Silva (Cornell University), Joël Ouaknine (MPI-SWS Saarbrücken), Andrzej Murawski (University of Oxford), Sebas- tian Junges (Radboud University Nijmegen), Guy Katz (The Hebrew University of Jerusalem), Christian Schilling (Aalborg University), Naijun Zhan (Peking University), Joost-Pieter Katoen (RWTH Aachen and University of Twente), Dirk Beyer (LMU Munich), Fabrice Kordon (Sorbonne University Paris), Laure Petrucci (Université Paris 13), Peter Y.A. Ryan (University of Luxembourg), Claudio Menghi (University of Berg- amo andMcMaster University Hamilton), Mark Lawford (McMaster University Hamil- ton), Maurice ter Beek (CNR-ISTI Pisa), Ferruccio Damiani (University of Turin), Kim Guldstrand Larsen (Aalborg University), Bernhard Beckert (KIT Karlsruhe), Mattias Ulbrich (KIT Karlsruhe), Reiko Heckel (University of Leicester), Vladimiro Sassone

ETAPS Foreword vii (University of Southampton), Anton Wijs (Eindhoven University of Technology), and Nikolai Kosmatov (Thales Research and Technology, Palaiseau). The ETAPS 2026 local organization team consisted of Maurice ter Beek (CNR- ISTI Pisa, general co-chair), Ferruccio Damiani (University of Turin, general co-chair), Barbara Boni (Synesthesia Turin, local organization chair), Vincenzo Ciancia (CNR- ISTI Pisa, satellite events co-chair), Luca Paolini (University of Turin, satellite events co-chair), Maria Tacconi (Synesthesia Turin, satellite events co-chair and publicity co- chair), Francesco Brocero (Synesthesia Turin, web co-chair and volunteers co-chair), José Proença (University of Porto, web co-chair), Gianluca Torta (University of Turin, publicity co-chair and local proceedings co-chair), Lucy James (Synesthesia Turin, sponsor chair), Giovanna Broccia (CNR-ISTI Pisa, local proceedings co-chair), Giorgio Audrito (University of Turin, volunteers co-chair), Riccardo Sieve (UiOOslo, volunteers co-chair), and Reiner Hähnle (TU Darmstadt, wine chair). I would like to take this opportunity to thank all authors, keynote speakers, invited tutorial speakers, and attendees. Special thanks goes to the organizers of the ETAPS 2026 satellite workshops and colocated events. ETAPS 2026 is grateful for the generous support of Amazon Web Services, AccessiWay, Camera di Commercio Industria Arti- gianato e Agricoltura di Torino, the Department of Computer Science of the University of Turin, Springer Nature, and Turismo Torino e provincia Convention Bureau. I thank our general co-chairs Maurice ter Beek (CNR-ISTI Pisa) and Ferruccio Damiani (Uni- versity of Turin), who made it all happen in Turin, and their local organization team for their enormous efforts to make ETAPS 2026 a fantastic event. I am especially grateful to Barbara Boni, Maria Tacconi, and Lucy James (Synesthesia Turin) for handling the organizational process in a smooth and reliable way. Last but not least, a big thanks to Jan Kofroň for all his help as an ETAPS Fellow and providing online presence support for the ETAPS conferences and the ETAPS Association. I hope you all enjoyed ETAPS 2026! April 2026 Laura Kovács ETAPS SC Chair, President of the ETAPS Association

Preface These proceedings volumes contain papers that were presented at the 35th European Symposium on Programming (ESOP 2026), held April 14–16 in Turin, Italy. ESOP is part of the International Joint Conferences on Theory and Practice of Software (ETAPS) and promotes the specification, design, analysis and implementation of programming languages and systems. In total, these two volumes contain 31 contributed papers and 1 invited paper. Fol- lowing recent editions of ESOP, ESOP 2026 had three submission categories: research papers, fresh perspectives, and experience reports. Of the 31 papers, these volumes con- tain 29 research papers and 2 experience reports. For the second time in its history, ESOP had two submission and evaluation rounds. The submission deadline of the first round was in June 2025, while the submission deadline of the second round was in October 2025. The first round attracted 38 submissions, of which 6 (16%) were immediately accepted, 23 (60%) were immediately rejected, and 9 (24%) were invited to submit a revised version in the second round. For submissions that were invited to submit a revi- sion, the program committee proposed concrete suggestions for improvement, and the revised submissions in the second round were reviewed by the same set of reviewers. The second round attracted 65 submissions, of which 9 were revisions from the first round, and 56 were entirely new submissions. Submissions in the second round were either immediately accepted or immediately rejected. Of the revisions submitted to the second round, 7were accepted (78%) and 2were rejected (22%). Of the new submissions submitted to the second round, 18 were accepted (32%) and 38 (68%) were rejected. In total, out of 94 unique submissions, 31 were accepted, yielding an acceptance rate of 33%. Submissions were reviewed in a double-blind fashion, with author identities only revealed to reviewers on definite paper acceptance. Submissions were typically reviewed by 3 program committee members. For some submissions, external reviewers pro- vided their expertise and insights through additional reviews. In total, every submission received at least 3 reviews, and in some cases 4 or 5 reviews. In both submission rounds, authors were allowed to submit an author response before the program committee dis- cussed and selected the papers asynchronously using the HotCRP system. Submissions for which the PC chair had a conflict of interest were kindly handled by Ilya Sergey. Similar to prior years, ESOP 2026 employed an artifact evaluation process. Of the 31 accepted papers, 17 elected to make their artifacts available on archival websites. The artifact committee awarded the badge “Functional” to 6 of these papers and the badges “Functional and Reusable” to 10 of these papers. My sincere thanks go to all whoworked together for ESOP 2026 and its proceedings. Foremost, I wish to thank the authors, who provided the technical content of the confer- ence. The program committee and external reviewers deserve particular thanks for their efforts in providing detailed reviews and participating in the discussions, and the artifact

x Preface evaluation committee for reviewing the accompanying artifacts. I thankMichael Samm- ler as the representative for ESOP among the artifact evaluation committee co-chairs. Finally, I would like to thank the ETAPS steering committee and its chair Laura Kovács, the proceedings coordinator Barbara König, the local proceedings chairs Gianluca Torta and Giovanna Broccia, and the webmaster Jan Kofroň for their assistance in the orga- nization of ESOP as a part of the entire ETAPS meeting. Finally, thanks are due to the members of the ESOP steering committee and, in particular, Luís Caires (SC chair) and Viktor Vafeiadis (PC chair 2025) for their advice and guidance. April 2026 Robbert Krebbers ESOP 2026 PC Chair

Organization Program Committee Chair Robbert Krebbers Radboud University Nijmegen, Netherlands Program Committee Alasdair Armstrong University of Cambridge, UK Aslan Askarov Aarhus University, Denmark Mohamed Faouzi Atig Uppsala University, Sweden Andrej Bauer University of Ljubljana, Slovenia Veronique Benzaken LMF Université Paris-Saclay, France Małgorzata Biernacka University of Wrocław, Poland Liang-Ting Chen Academia Sinica, Taiwan Raphaëlle Crubillé Aix Marseille Univ, CNRS, LIS, France Deepak D’Souza Indian Institute of Science, India Ankush Das Boston University, USA Farzaneh Derakhshan Illinois Institute of Technology, USA Emanuele D’Osualdo University of Konstanz, Germany Paulo Emílio de Vilhena Imperial College London, UK Francesco Gavazzo University of Padua, Italy Justin Hsu Cornell University, USA Ambrus Kaposi Eötvös Loránd University, Hungary Sven Keidel TU Darmstadt, Germany Ori Lahav Tel Aviv University, Israel Christoph Matheja University of Oldenburg, Germany and DTU Compute, Denmark Andreia Mordido LASIGE, University of Lisbon, Portugal Christopher Pulte University of Cambridge, UK Jorge A. Pérez University of Groningen, Netherlands Ryosuke Sato Tokyo University of Agriculture and Technology, Japan Ilya Sergey National University of Singapore, Singapore Kathrin Stark Heriot-Watt University, UK Bernardo Toninho NOVA FCT and NOVA LINCS, Portugal Jana Wagemaker Radboud University Nijmegen, Netherlands John Wickerson Imperial College London, UK Fabio Zanasi University College London, UK

xii Organization ESOP/FASE/FoSSaCS Joint Artifact Evaluation Committee Chairs Michael Sammler ISTA, Austria Yannic Noller Ruhr University Bochum, Germany Guillermo Alberto Perez University of Antwerp, Belgium ESOP/FASE/FoSSaCS Joint Artifact Evaluation Committee Mohammad Afzal TCS Research and IIT Bombay, India Flavio Ascari University of Konstanz, Germany Aren A. Babikian University of Toronto, Canada Alexander Bai New York University, USA David Boetius University of Konstanz, Germany Michaël Cadilhac DePaul University, USA Ronaldo Canizales Colorado State University, USA William Eiers Stevens Institute of Technology, USA Kasper Engelen University of Antwerp, Belgium Máté Földiák Linköping University, Sweden Alvin George IISc Bangalore, India Holly Hendry University of York, UK Martin Kristjansen Aalborg University, Denmark Andrea Laretto Tallinn University of Technology, Estonia Megan Maton University of Sheffield, UK Logan Murphy University of Toronto, Canada Olek Osikowicz University of Sheffield, UK Jan-Paul Ramos-Dávila Boston University, USA Wojciech Rozowski Lean FRO, USA Chia Sabah University of Leicester, UK William Scarbro Colorado State University, USA Hitarth Singh Hong Kong University of Science and Technology, Hong Kong Steffan Sølvsten Aarhus University, Denmark Stephan Spengler Uppsala University, Sweden Gaëtan Staquet École Centrale Nantes, France Abhishek U IISc, India Alexandra van der Spuy Stellenbosch University, South Africa Szumi Xie Eötvös Loránd University, Hungary Ekaterina Zhuchko Tallinn University of Technology, Estonia

Organization xiii ESOP Steering Committee Luís Caires (Chair) Instituto Superior Técnico, Universidade de Lisboa, Portugal Robbert Krebbers Radboud University Nijmegen, Netherlands Brigitte Pientka McGill University, Canada Azalea Raad Imperial College London, UK Viktor Vafeiadis MPI-SWS, Germany Stephanie Weirich University of Pennsylvania, USA Nobuko Yoshida University of Oxford, UK Additional Reviewers Flavio Ascari Lara Bargmann Albert Benvenistea Elie Bermot Victor Blanchi Richard Bubel Tej Chajed James Cheney Claudio Sacerdoti Coen Pierre-Evariste Dagand Ryan Doenges Vorashil Farzaliyev Roberto Giacobazzi Peter Habermehl Jan Hoffmann Johannes Hostert Jules Jacobs Swen Jacobs Matan Kalp Maja H. Kirkeby Aleks Kissinger Quang Loc Le Leo Lobski Raz Lotan Kenji Maillard Vaibhav Mehta Magnus Myreen Max New Jennifer Paykin Daniel Pelsmaeker Roberto Pettinau Frank Pfenning Robin Piedeleu Nicolò Pizzo Francois Pottier Damien Pous Enguerrand Prebet Ralph Sarkis Rahul Sharma Stephen F. Siegel Zachary Tatlock Mateo Torres-Ruiz David Trabish Renaud Vilmart Uwe Waldmann Mingsheng Ying Vladimir Zamdzhiev

Contents Formal Methods meet Digital Twins: Challenges and Opportunities . . . . . . . . . . . 1 Einar Broch Johnsen, Eduard Kamburjan, Andrea Pferscher, and Silvia Lizeth Tapia Tarifa Contextual Metaprogramming for Session Types . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Pedro Ângelo, Atsushi Igarashi, Yuito Murase, and Vasco T. Vasconcelos Specifying and Verifying RDMA Synchronisation . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Guillaume Ambal, Max Stupple, Brijesh Dongol, and Azalea Raad In Cantor Space No One Can Hear You Stream . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot Deciding not to Decide: Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 Patrycja Balik, Szymon Jędras, and Piotr Polesiuk Recursive Logical Relations for Intuitionistic Linear Logic Session Types . . . . . 135 Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, and Yue Yao Code Generation via Meta-programming in Dependently Typed Proof Assistants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166 Mathis Bouverot-Dupuis and Yannick Forster Linear Effects, Exceptions, and Resource Safety: A Curry-Howard Correspondence for Destructors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 190 Sidney Congard, Guillaume Munch-Maccagnoni, and Rémi Douence Rely-Guarantee Is Coinductive – A Proof-Centered Investigation of Inductively Approximated Coinduction – . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 220 John Derrick, Chelsea Edmonds, Andrei Popescu, and Jamie Wright Reduction for Structured Concurrent Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 252 Namratha Gangamreddypalli, Constantin Enea, and Shaz Qadeer Specification-Driven Generation of Summaries for Symbolic Execution . . . . . . . 283 Rafael Gonçalves, Frederico Ramos, Pedro Adão, and José Fragoso Santos

xvi Contents Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 314 Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg, and Tobias Winkler A Program Logic for Under-approximating Worst-case Resource Usage . . . . . . . 344 Ziyue Jin and Di Wang Causal-Broadcast Memory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 373 Amir Karniel and Ori Lahav A Category-Theoretic Framework for Dependent Effect Systems . . . . . . . . . . . . . 401 Satoshi Kura, Marco Gaboardi, Taro Sekiyama, and Hiroshi Unno Validating Quantum State Preparation Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . 432 Liyi Li, Anshu Sharma, Zoukarneini Difaizi Tagba, Sean Frett, and Alex Potanin The Memorist Tale: Every Thunk Every Cost All At Once . . . . . . . . . . . . . . . . . . . 463 Xing Li, Yao Li, Peter Schachte, and Christine Rizkallah Author Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 493

Formal Methods meet Digital Twins: Challenges and Opportunities Einar Broch Johnsen1 , Eduard Kamburjan2,1 , Andrea Pferscher1 , and Silvia Lizeth Tapia Tarifa1 1 University of Oslo, Oslo, Norway {einarj,andreapf,sltarifa}@uio.no 2 IT University of Copenhagen, Copenhagen, Denmark eduard.kamburjan@itu.dk Abstract. The advent of digital twins gives us an opportunity to re- flect on the relationship between models and modelled systems. We may think of digital twins not merely as models, but as systems for model management, integration, and composition. In fact, digital twins are model-centric systems that maintain a two-way connection between an ecosystem of models and the modelled system, realised through streams of observations and streams of interventions. This connection introduces agility as the digital twin can typically both adapt its models on-the-fly to changes in a modelled system and influence the modelled system’s behaviour. In this paper, we discuss key concepts of digital twins from a formal methods perspective and suggest opportunities and challenges for formal methods in digital twin systems. In particular, we consider how formal techniques can be integral to the digital twin, both in terms of digital twin technology and in terms of digital twin models, as well as notions of correctness for the digital twin itself. 1 Introduction Today, digital twins (DTs) are subject to a fair amount of hype1 for their poten- tial to improve efficiency and mitigate failure in a broad range of systems, during system operation. DTs are a key concept in Industry 4.0 [10,54]; applications of DTs are found across engineering disciplines, based on the idea of creating an increasingly accurate “virtual replica” of a cyber-physical system to predict be- haviour by means of sophisticated simulation techniques and a closed feedback loop to the actual system (e.g., [15]). DTs are now increasingly found in ap- plication domains beyond engineering, including medicine [42], healthcare [55], energy [44], manufacturing [6,40], transportation [11], and software systems [1]. DTs are useful to explain unexpected incidents, for short-term decision- making and for long-term strategic planning. To this aim, a DT can have the ability to deliver different analytical services, including historical analysis (what 1 https://www.weforum.org/stories/2024/06/digital-twins-and-industrial-clusters- are-about-to-change-the-face-of-manufacturing/ © The Author(s) 2026 R. Krebbers (Ed.): ESOP 2026, LNCS 16501, pp. 1–12, 2026. https://doi.org/10.1007/978-3-032-22720-1_1

2 E. B. Johnsen et al. happened in the past), descriptive analysis (what just happened), predictive analysis (what do we expect to happen next), prescriptive/proactive analysis (strategic planning, what can we do to change the expected behaviour), and reactive analysis (provide an immediate response for what to do now). DTs realise these services by enabling a target system and its models to in- teract at runtime; e.g., models in the DT and observations from the real system work together to drive analytical services. Conceptually, DTs represent a shift from model-based to model-centric system design, and hence from a correctness- preserving perspective on system construction to a correctness-adapting per- spective on system maintenance. The models and our ability to automatically analyse them, are integral to the target system, rather than a means to develop this target system. Consequently, the lifetime of a DT matches the lifetime of the actual system: we may need the ability to automatically adapt our models when these need better alignment with observed data from the actual system, and to analyse new or adapted models on-the-fly. Formal methods are different techniques to mathematically specify and ver- ify system behaviour, in which systems are modelled as mathematically defined structures [5, 60, 61]; these methods are interesting for the strength of the guar- antees they can provide, allowing the presence (or absence) of a particular be- haviour to be mathematically proven for the given model. Thus, formal methods are complementary to testing- or simulation-based analysis techniques [20]. For- mal methods can be applied at different stages of system design. In terms of indus- trial applications, formal methods have traditionally been used for safety-critical applications, but there is an increasing uptake in other domains [5, 16]. In this paper, we argue that DTs may be of significant interest to developers of formal methods and that DTs give us an opportunity to revisit how we think formal models may be developed and used. We consider two perspectives on how formal methods and DTs can come together: how formal methods can be used as components in DTs (Sect. 3) and how formal methods can be used to analyse DTs (Sect. 4). For each perspective, we outline some open research challenges related to DTs and formal methods in a broad sense, and hint at how we have started to approach these challenges in our own work. 2 What are Digital Twins? DTs are virtual information constructs that capture the structure, context, and behaviour of the system they are twinning, are dynamically updated with data from the actual system, have predictive capability, and inform decisions that realise value, according to a recent definition by the National Academy for Sci- ence, Engineering and Medicine (NASEM) [46]. This notion of a DT puts less weight on bidirectionality (i.e., the reactive control of a cyber-physical system) and emphasises the tight integration between a model and the modelled system to provide services for, e.g., analysis, diagnosis, prediction, fault detection and strategic planning [43].

Formal Methods meet Digital Twins: Challenges and Opportunities 3 An essential aspect of a DT is its life cycle: DTs are intended to be long-lived systems. Often, the DT predates the target system as a design or construction artefact that is later transformed into an operational tool, and may persist also after the actual system has ceased to operate. It closely mimics the life cycle of the actual system; specifically, this means that it needs to adapt its models to changes in its environment, which can include both the actual system and the requirements to the actual system. In fact, the user requirements to the DT may also change over the lifetime of the DT [43]; i.e., the purpose of the DT is likely to evolve over time. This way, the DT becomes a self-adaptive system for advanced model management, generating and adjusting its models and determining the analyses to be performed using these models on-the-fly. A self-adaptive system typically consists of a managed and a managing layer, often organised as a MAPE-K feedback loop [58], in which monitor-, analyse-, plan- and execute-components interact with a knowledge base. The knowledge base is often used to provide a context for the MAPE-components, capturing, e.g., historical data, domain knowledge and requirements. While the DT can be seen as a managing layer for its target system, self-adaptation within the DT can be addressed by adding an additional layer of self-adaptation to capture how the twin itself evolves over time [29], see Fig. 1. Remark that the knowledge base may include so-called runtime models [9] that blur the distinction between software development and execution [4], enabling introspection in support of the self-adaptation process. The purpose of behavioural self-adaptation in Layer 1 is to control how the current models of the DT capture the behaviour of the actual system (thus addressing the so-called real-to-sim or reality gap, e.g. [7, 56, 62]) and make adjustments to the actual system if needed. In the feedback loop of Layer 1, the monitor collects data from the sensors connected to the actual system, the analyser assesses whether these observations of the actual system comply with requirements, the planner determines whether changes to the actual system are needed and the executor manipulates the actuators to influence the behaviour of the actual system. The purpose of structural self-adaptation in Layer 2 is to control how the DT captures the structure and context of the actual system. In the feedback loop of Layer 2, the analyser determines that the requirements to the actual system have changed, that the targeted behaviour is different and that the means to achieve this behaviour are no longer the same, leading to changes in the components of Layer 1 of the DT, including its models. 3 Formal Methods in Digital Twins Let us first consider how formal methods can be integrated in the analysis ser- vices of the DT. One important aspect of this integration, is that we are dealing with an open environment : we do not assume that the models perfectly reflect the actual system. Instead, analysis inside the DT is data-driven; i.e., the model configuration at a given point in time depends on the stream of observations

4 E. B. Johnsen et al. Knowledge Base Layer 1 PlannerLayer 1 Analyser Layer 1 Executor Layer 2 PlannerLayer 2 Analyser Layer 2 Executor Actual SystemSensors Actuators Monitor Architectural self- adaptation (blue) Behavioural self- adaptation (gray) Managed system Fig. 1. A two-layered self-adaptive DT architecture with MAPE-K feedback loops for behavioural (Layer 1, gray) and architectural (Layer 2, blue) self-adaptation. that the twin receives from the actual system. Hence, our methods need to sup- port the dynamic configuration and composition of models reflecting the current structure and observed state of the actual system. The DT needs a strategy for how that should be done, depending on the analysis service it delivers. Challenge 1 How can formal models be dynamically configured and composed? We can understand a DT as a model management system that, driven by streams of observations of the actual system, uses contextual information to decide how to configure its models to deliver analysis services. We can build on the experiences from model management systems for consistency [52], and consider formal methods from this perspective as well. If we assume that the contextual information is captured in its knowledge base, we can see the DT as a model orchestrator that can compose different models. Simulation models can be orchestrated using co-simulation algorithms [17], and dynamically deployed [19]. Similar workflows may be conceived to configure and compose heterogeneous formal models, and their corresponding analyses. For example, BedreFlyt [35,51] is a DT for hospital ward planning that uses incoming patient data as its stream of observations from the ward and information about treatments stored in the knowledge base to dynamically configure and deploy an actor-model in ABS [28], which outputs a stream of resource requirements reflecting day-to-day bed bay needs for the patients in the ward. These are, together with constraints on bed bay capacity in the ward derived from the knowledge base, used to dynamically configure a stream of optimisation problems, which are given to Z3 [8]. The twin’s output is a stream of bed bay allocations that can be given to the ward’s admitting nurse. This way, the twin combines several formal methods. Challenge 2 How can formal methods help in automatically adapting digital twin models to life cycle changes in the target system? We all know how challenging it can be to manually create adequate formal models [60]. Already for standardised communication protocols, ambiguities al- low for different behaviours, which may require different model representations;

Formal Methods meet Digital Twins: Challenges and Opportunities 5 this suggests that incremental approaches are needed in an open world setting in which not all behaviours are known in advance [41]. Manually modelling all these different representations would be tedious and error-prone. Here, one interesting direction is to explore model learning [53], a technique to automatically generate finite state models from system traces, to automatically generate and test models in the model ecosystem of DTs [47,57]. However, for bilateral synchronisation be- tween the DTs and real system, the underlying models must reflect the behaviour of the actual system. One way to address this problem can be to use techniques from probabilistic model checking [3] to support the model management process of the DT in selecting models based on the current environment [38]. Challenge 3 How can formal methods enhance a digital twin by providing ad- vanced behavioural insights into its target system? Formal methods can provide worst-case analyses as well as statistical guar- antees not readily available with symbolic or mechanistic models. Given that the actual system is not fully understood, or that it operates in an uncontrolled environment, it seems interesting to not only analyse these streams using expres- sive runtime verification techniques [39], but also to investigate the generation of such analysis problems on-the-fly, driven by the stream of observations from the actual system. As a step in this direction, we have explored the use of model checking techniques over sliding window segments of event streams to analyse how properties of learnt models evolve over time [36,37]. Another interesting re- search direction is to use formal specifications to define input scenarios amenable to a hypothetical (what-if) analysis; e.g., in the BedreFlyt DT, we have used this kind of techniques to analyse average case and worst-case resource usage for bed- bay allocation in a hospital ward [35]. 4 Formal Methods for Digital Twins Let us next consider formal methods for the overall DT architecture and focus on the DT’s need to be dynamically updated, driven by data from the actual sys- tem, i.e., its self-adaptive capabilities. Early work on formal methods to model and analyse self-adaptive systems was surveyed by Weyns et al. [59], who re- ports a “remarkably low” number of papers on this topic. By structuring the configuration space of the self-adaptive system, self-adaptation has connections to variability and especially to dynamic software product lines [18, 21] in the sense that they provide a means to reconfigure the system between different configurations. While software product lines have been formalised using, e.g., featured transition systems [13], formal methods for dynamic software product lines have received less attention [49]. However, tools such as ProFeat [12], which supports family-based model-checking with a feature controller that can activate and deactivate features in the configuration space, have been used to formally model and analyse self-adaptive systems (e.g., [48]). Early work on the modelling and analysis of MAPE-K feedback loops essen- tially treated the knowledge base as a shared memory between processes [2,23].