|
Published: 30th October 2024 DOI: 10.4204/EPTCS.409 ISSN: 2075-2180 |
This volume contains the proceedings of GandALF 2024, the Fifteenth International Symposium on Games, Automata, Logics, and Formal Verification. The symposium was held in Reykjavik, Iceland, on June 19-21, 2024.
The GandALF symposium was established to provide an opportunity for researchers interested in logic for computer science, automata theory, and game theory, to gather and discuss the application of formal methods to the specification, design, and verification of complex systems. Previous editions of GandALF were held in Udine, Italy (2024); Madrid, Spain (2022); Padova, Italy (2021); Brussels, Belgium (2020); Bordeaux, France (2019); Saarbrücken, Germany (2018); Rome, Italy (2017); Catania, Italy (2016); Genoa, Italy (2015); Verona, Italy (2014); Borca di Cadore, Italy (2013); Napoli, Italy (2012); and Minori, Italy (2011 and 2010). The symposium provides an international forum where people from different areas, backgrounds, and countries, can fruitfully interact, as witnessed by the composition of the program and steering committees and by the country distribution of the submitted papers.
The program committee selected 10 papers (out of 20 submissions) for presentation at the symposium. Each paper was reviewed by at least three referees, and the selection was based on originality, quality, and relevance to the topics of the call for papers. The scientific program included presentations on automata, logics for computer science and verification, learning for verification, formal methods and specification languages, games for security and verification, session types, and synthesis. The program included four invited talks, given by Bernd Finkbeiner (CISPA Helmholtz Center for Information Security), Kim G. Larsen (Aalborg University), Brigitte Pientka (McGill University), and Azalea Raad (Imperial College London). We are deeply grateful to them for contributing to this year's edition of GandALF.
We would like to thank the authors who submitted papers, the speakers, the program committee members, and the additional reviewers for their excellent work. We also thank EPTCS and arXiv for hosting the proceedings; in particular, we thank Rob van Glabbeek for the precise and prompt technical support with issues related to the proceeding publication procedure.
Finally, we would like to thank the local organisers: Angeliki Chalki, Jana Wagemaker, Vasiliki Kyriakou, and Jasmine Xuereb for ensuring the event ran smoothly.
Antonis Achilleos and Adrian Francalanza
Luca Geatti, Karam Kharraz, Paolo Marrone, Piotr Polesiuk, Nicola Prezza, Christian Schilling, Daniel Thoma, Alexander Weinert.
System requirements related to concepts like information flow, knowledge, and robustness cannot be judged in terms of individual system executions, but rather require an analysis of the relationship between multiple executions. Such requirements belong to the class of hyperproperties, which generalize classic trace properties to properties of sets of traces.
A key idea in the verification of hyperproperties has been to analyze self-compositions of programs. Hyperproperties that need to hold for all possible combinations of k traces, such as k-hypersafety properties, can be analyzed as standard trace properties of the k-fold self-composition. The implicit universal quantification over the traces is, however, an inherent limitation of this paradigm, which makes it difficult to abstract in an existential manner from phenomena like scheduling in concurrent programs, nondeterministic choice, or speed of execution in asynchronous computations. Alternations between quantifiers are furthermore essential for counterfactual reasoning about causation and blame.
In this talk, we will explore the exciting world of hyperproperties beyond k-hypersafety. I will discuss the decidability and complexity of reasoning about such hyperproperties and present algorithmic techniques for the effective resolution of quantifier alternations. I will also give an overview of recently introduced logics for the specification of hyperproperties beyond k-hypersafety, including logics that combine hyperproperties with reasoning over strategies, and logics for second-order hyperproperties.
I will present recent advances and applications of the tool UPPAAL Stratego (www.uppaal.org) supporting automatic synthesis of guaranteed safe and near-optimal control strategies for cyber physical systems. UPPAAL Stratego support reinforcement learning methods to construct near-optimal controllers. However, their behavior is not guaranteed to be safe, even when it is encouraged by reward engineering. One way of imposing safety to a learned controller is to use a safety shield, synthesized using symbolic methods from checking, and hence correct by design. To make synthesis of shields for hybrid environments tractable UPPAAL Stratego are using various abstraction techniques for hybrids systems.
We study the impact of the synthesized shield when applied as either a pre-shield (applied before learning a controller) or a post-shield (only applied after learning a controller). In addition trade-offs between efficiency of strategy representation and degree of optimality subject to safety constraints will be discussed, as well as successful on-going applications (water-management, heating systems, and traffic control).
Process calculi provide a tool for the high-level description of interactions, communications, and synchronizations between a collection of independent processes. Session types allow us to statically verify that processes communicate according to prescribed protocols. Hence, they rule out a wide class of communication-related bugs before executing a given process. They also statically guarantee safety properties such as session fidelity and deadlock freedom, analogous to preservation and progress in the simply typed lambda-calculus.
Although there have been many efforts to mechanize process calculi such as the pi-calculi in proof assistants, mechanizing these systems remains an art. Process calculi use channel or action names to specify process interactions, and they often feature rich binding structures and semantics such as channel mobility. Both of these features can be challenging to mechanize, for we must track names to avoid conflicts, ensure that α-equivalence and renaming are well-defined, etc. Moreover, session types employ a linear type system, where variables cannot be implicitly copied or dropped, and therefore, many mechanizations of these systems require modeling the context and carefully ensuring that its variables are handled linearly.
In this talk, I give an introduction to the challenges that arise when mechanizing session types, and showcase two different kinds of solutions focusing on a session typed system based on classical linear logic: first, I show how to mechanize the a session tysystem directly using explicit contexts identifying key context operations to manage linear contexts; then I show a technique to localize linearity conditions as additional predicates embedded within type judgments, which allows us to use unrestricted typing contexts instead of linear ones. This latter technique is especially relevant when leveraging (weak) higher-order abstract syntax to defer the intricate channel mobility and bindings that arise in a session typed system.
From this mechanization, we discuss key design decisions and draw some key lessons for mechanizing substructural systems, such as session types. The goal of this talk is to engage the community in discussions on what support in proof environments is needed to support the mechanization of substructural systems.
This is joint work with Chuta Sano, Daniel Zackon, Ryan Kavanagh, and Alberto Momigliano.
Incorrectness Logic (IL) has recently been advanced as a logical under-approximate theory for proving the presence of bugs-dual to Hoare Logic, which is an over-approximate theory for proving the absence of bugs. To facilitate scalable bug detection, we developed incorrectness separation logic (ISL) by marrying the under-approximate reasoning of IL with the local reasoning of separation logic. This locality leads to techniques that are compositional both in code (concentrating on a program component) and in the resources accessed (spatial locality), without tracking the entire global state or the global program within which a component sits. This enables reasoning to scale to large teams and codebases: reasoning can be done even when a global program is not present. To demonstrate this, we developed Pulse, an automatic program analysis for catching memory safety errors, underpinned by ISL. Using Pulse, deployed at Meta, we found a number of real bugs in large codebases such as OpenSSL.
Inspired by this success, we later studied the power of under-approximation for detecting non-termination bugs. Program termination is a classic non-safety property that cannot in general be witnessed by a finite trace. This makes testing for non-termination challenging, and also makes it a natural target for symbolic proof. Discovering non-termination is an under-approximate problem. We thus developed an under-approximate logic for proving non-termination, resulting in a compositional proof method. We prototyped this in an automated tool, Pulse∞ (an extension of Pulse), which has already discovered a number of non-termination bugs in large open-source libraries.