<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">
<div>[apologies for multiple copies]</div>
<div><br>
</div>
<div><br>
</div>
<div>*****************************************************************************************************</div>
<div>Call for Partecipation - GandALF 2025</div>
<div>*****************************************************************************************************</div>
<div><br>
</div>
<div>The Sixteenth International Symposium on Games, Automata, Logics, and Formal Verification </div>
<div>will take place in Valletta, Malta, 16-17 September 2025.</div>
<div><br>
</div>
<div>Web page: https://gandalfsymposium.github.io/2025/</div>
<div><br>
</div>
<div>The aim of the symposium is to bring together researchers from</div>
<div>academia and industry which are actively working in the fields of</div>
<div>Games, Automata, Logics, and Formal Verification. The symposium covers</div>
<div>an ample spectrum of themes, ranging from theory to applications, and</div>
<div>encourages cross-fertilization. Papers focused on formal methods are</div>
<div>especially welcome. Authors are invited to submit original research or</div>
<div>tool papers on all relevant topics in these areas. Papers discussing</div>
<div>new ideas that are at an early stage of development are also welcome.</div>
<div><br>
</div>
<div>The topics covered by the conference include, but are not limited to,</div>
<div>the following:</div>
<div><br>
</div>
<div>Automata Theory</div>
<div>Automated Deduction</div>
<div>Computational aspects of Game Theory</div>
<div>Concurrency and Distributed computation</div>
<div>Decision Procedures</div>
<div>Deductive, Compositional, and Abstraction Techniques for Verification</div>
<div>Finite Model Theory</div>
<div>First-order and Higher-order Logics</div>
<div>Formal Languages</div>
<div>Formal Methods for Systems Biology, Hybrid, Embedded, and Mobile Systems</div>
<div>Games and Automata for Verification</div>
<div>Game Semantics</div>
<div>Logical aspects of Computational Complexity</div>
<div>Logics of Programs</div>
<div>Modal and Temporal Logics</div>
<div>Model Checking</div>
<div>Models of Reactive and Real-Time Systems</div>
<div>Program Analysis and Software Verification</div>
<div>Run-time Verification and Testing</div>
<div>Specification and Verification of Finite and Infinite-state Systems Synthesis</div>
<div><br>
</div>
<div>## Invited Speakers:</div>
<div><br>
</div>
<div>- Radu Mardare (Heriot-Watt University, Edinburgh, Scotland)</div>
<div>- Simon Fowler (University of Glasgow, Glasgow, Scotland)</div>
<div><br>
</div>
<div>## Important dates:</div>
<div><br>
</div>
<div>Early registration deadline: 30 July 2025</div>
<div>Conference dates: 16-17 September 2025</div>
<div><br>
</div>
<div>## Venue:</div>
<div><br>
</div>
<div>The Valletta Campus, originally built as a Jesuit College, began construction in 1595 under Grand </div>
<div>Master Martino Garzes. Located between St. Paul, St. Christopher, Merchants, and Archbishop Streets, </div>
<div>the building features Renaissance architecture with a central courtyard. The Jesuit church, part of </div>
<div>the complex, was built between 1592 and 1609. Initially plain, the facade was redesigned in the </div>
<div>Baroque style around 1647 by architect Francesco Buonamici. </div>
<div>The interior boasts an ornate ceiling, a historic staircase, and portrait-lined corridors. Some current </div>
<div>offices were once Jesuit priests’ cells. The building suffered major damage in a 1634 explosion and </div>
<div>the 1693 earthquake, leading to various reconstructions. Notable additions included a sundial (1695) </div>
<div>and a courtyard clock, both with Latin inscriptions.</div>
<div>After the Jesuits were expelled in 1768, the Order of St. John took over, maintaining education. </div>
<div>In 1769, a formal University was established, re-inaugurated in 1779. During French rule (1798–1800), </div>
<div>the building became the École Centrale, with scientific and educational functions. The British later </div>
<div>restored the University and added a Doric-style entrance in 1824. The building was used for various purposes, </div>
<div>including a WWII air raid center and offices such as the Anglo-Maltese Library and Heritage Malta.</div>
<div>Today, it hosts several institutions, including the CEU, RIDT, Conflict Resolution Centre, and the </div>
<div>International Institute for Justice and the Rule of Law.</div>
<div><br>
</div>
<div>## Accepted papers:</div>
<div><br>
</div>
<div>- Dylan Leveille: </div>
<div> Generating Plans for Belief-Desire-Intention (BDI) Agents Using Alternating-Time Temporal Logic (ATL)</div>
<div>- Luca Aceto, Antonis Achilleos, Aggeliki Chalki, and Anna Ingolfsdottir: </div>
<div> The Complexity of Deciding Characteristic Formulae Modulo Nested Simulation</div>
<div>- Purandar Bhaduri: </div>
<div> The Complexity of Pure Strategy Relevant Equilibria in Concurrent Games</div>
<div>- Gaëtan Regaud and Martin Zimmermann: </div>
<div> The Complexity of Generalized HyperLTL with Stuttering and Contexts</div>
<div>- Muqsit Azeem, Jan Kretinsky, and Maximilian Weininger: </div>
<div> Sound Value Iteration for Simple Stochastic Games</div>
<div>- Rüdiger Ehlers: </div>
<div> How Concise are Chains of co-Büchi Automata?</div>
<div>- Michele Boreale and Luisa: </div>
<div> Collodi Parallelizable Feynman-Kac models for universal probabilistic programming</div>
<div>- Massimo Benerecetti, Dario Della Monica, Angelo Matteo, Fabio Mogavero, and Gabriele Puppis: </div>
<div> Automaton-based Characterisation of First Order Logic over Infinite Trees</div>
<div>- Sougata Bose, Daniel Hausmann, Soumyajit Paul, Sven Schewe, and Tansholpan Zhanabekova: </div>
<div> Generalised Reachability Games Revisited</div>
<div>- Radu Mardare, Neil Ghani, and Eigil Rischel: </div>
<div> Metric Equational Theories</div>
<div><br>
</div>
<div>## Program Committee:</div>
<div><br>
</div>
<div>Elli Anastasiadi (Aalborg University)</div>
<div>Giorgio Bacci (Aalborg University) co-Chair</div>
<div>Giovanni Bernardi (Université Paris Diderot - IRIF)</div>
<div>Udi Boker (Reichman Universtiy)</div>
<div>Sougata Bose (University of Mons)</div>
<div>Laure Daviaud (University of East Anglia)</div>
<div>Abhishek De (University of Birmingham)</div>
<div>Angelo Ferrando (University of Modena and Reggio Emilia)</div>
<div>Mohammed Foughali (IRIF/Université Paris Cité)</div>
<div>Adrian Francalanza (University of Malta) co-Chair</div>
<div>Silvia Ghilezan (University of Novi Sad)</div>
<div>Mirco Giacobbe (University of Birmingham)</div>
<div>Daniele Gorla (University of Rome "La Sapienza")</div>
<div>Ross Horne (University of Strathclyde)</div>
<div>Ryan Kavanagh (Université du Québec à Montréal)</div>
<div>Marina Lenisa (University of Udine)</div>
<div>Tim Lyon (Technische Universität Dresden)</div>
<div>Konstantinos Mamouras (Rice University)</div>
<div>Mohammad Reza Mousavi (King's College London)</div>
<div>Ocan Sankur (Mitsubishi Electric R&D Centre Europe)</div>
<div>Sarah Winkler (Free University of Bozen-Bolzano)</div>
<div>Sarah Winter (Université Paris Cité - IRIF)</div>
<div><br>
</div>
<div>## Steering Committee:</div>
<div><br>
</div>
<div>Luca Aceto (Reykjavik University)</div>
<div>Javier Esparza (University of Munich)</div>
<div>Salvatore La Torre (University of Salerno)</div>
<div>Angelo Montanari (University of Udine)</div>
<div>Mimmo Parente (University of Salerno)</div>
<div>Jean-François Raskin (Université libre de Bruxelles)</div>
<div>Martin Zimmermann (Aalborg University)</div>
<div>
<div class="Box-sc-g0xbh4-0 kHHiZS" style="box-sizing: border-box; pointer-events: none;">
<div tabindex="0" class="Box-sc-g0xbh4-0 jqUoVd" style="box-sizing: border-box; overflow-x: overlay;">
<div class="Box-sc-g0xbh4-0 bZMwND react-code-file-contents" role="presentation" aria-hidden="true" data-tab-size="8" data-paste-markdown-skip="true" data-hpc="true" style="box-sizing: border-box; display: flex; tab-size: 8; position: relative; width: 1374px; max-width: unset;">
<div class="react-line-numbers-no-virtualization" style="box-sizing: border-box; position: relative; z-index: 2; display: flex; width: 82px; min-width: 82px; pointer-events: auto; flex-direction: column; align-items: flex-end;">
<div class="react-no-virtualization-wrapper-lines" style="box-sizing: border-box; contain-intrinsic-height: auto 1200px; padding-right: 10px; color: rgb(31, 35, 40); font-family: -apple-system, system-ui, "Segoe UI", "Noto Sans", Helvetica, Arial, sans-serif, "Apple Color Emoji", "Segoe UI Emoji"; font-size: 14px; font-variant-ligatures: normal; orphans: 2; widows: 2; background-color: rgb(255, 255, 255); text-decoration-thickness: initial; text-decoration-style: initial; text-decoration-color: initial;">
</div>
<div class="react-no-virtualization-wrapper-lines" style="box-sizing: border-box; contain-intrinsic-height: auto 1200px; padding-right: 10px; color: rgb(31, 35, 40); font-family: -apple-system, system-ui, "Segoe UI", "Noto Sans", Helvetica, Arial, sans-serif, "Apple Color Emoji", "Segoe UI Emoji"; font-size: 14px; font-variant-ligatures: normal; orphans: 2; widows: 2; background-color: rgb(255, 255, 255); text-decoration-thickness: initial; text-decoration-style: initial; text-decoration-color: initial;">
</div>
<br class="Apple-interchange-newline">
</div>
<div class="react-line-numbers-no-virtualization" style="box-sizing: border-box; position: relative; z-index: 2; display: flex; width: 82px; min-width: 82px; pointer-events: auto; flex-direction: column; align-items: flex-end;">
<div class="Box-sc-g0xbh4-0 kHHiZS" style="box-sizing: border-box; pointer-events: none;">
<div tabindex="0" class="Box-sc-g0xbh4-0 jqUoVd" style="box-sizing: border-box; overflow-x: overlay;">
<div class="Box-sc-g0xbh4-0 bZMwND react-code-file-contents" role="presentation" aria-hidden="true" data-tab-size="8" data-paste-markdown-skip="true" data-hpc="true" style="box-sizing: border-box; display: flex; tab-size: 8; position: relative; width: 1374px; max-width: unset;">
<div class="react-line-numbers-no-virtualization" style="box-sizing: border-box; position: relative; z-index: 2; display: flex; width: 82px; min-width: 82px; pointer-events: auto; flex-direction: column; align-items: flex-end;">
<div class="react-no-virtualization-wrapper-lines" style="box-sizing: border-box; contain-intrinsic-height: auto 1200px; padding-right: 10px; color: rgb(31, 35, 40); font-family: -apple-system, system-ui, "Segoe UI", "Noto Sans", Helvetica, Arial, sans-serif, "Apple Color Emoji", "Segoe UI Emoji"; font-size: 14px; font-variant-ligatures: normal; orphans: 2; widows: 2; background-color: rgb(255, 255, 255); text-decoration-thickness: initial; text-decoration-style: initial; text-decoration-color: initial;">
</div>
<div class="react-no-virtualization-wrapper-lines" style="box-sizing: border-box; contain-intrinsic-height: auto 1200px; padding-right: 10px; color: rgb(31, 35, 40); font-family: -apple-system, system-ui, "Segoe UI", "Noto Sans", Helvetica, Arial, sans-serif, "Apple Color Emoji", "Segoe UI Emoji"; font-size: 14px; font-variant-ligatures: normal; orphans: 2; widows: 2; background-color: rgb(255, 255, 255); text-decoration-thickness: initial; text-decoration-style: initial; text-decoration-color: initial;">
</div>
<br class="Apple-interchange-newline">
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</body>
</html>