Abstract Introduction Citation for Gaëtan Douéneau-Tabot Citation for Aliaume Lopez Jury Previous winners

The Ackermann Award 2024

Maribel Fernández ORCID Department of Informatics, King’s College London, UK Prakash Panangaden McGill University, Canada
Abstract

Report on the 2024 Ackermann Award.

Keywords and phrases:
finite automaton, string transducer, class membership problem, first-order logic, preservation theorem, finite model theory
Category:
Ackermann Award
Copyright and License:
[Uncaptioned image] © Maribel Fernández and Prakash Panangaden; licensed under Creative Commons License CC-BY 4.0
2012 ACM Subject Classification:
Theory of computation → Logic and verification ; Theory of computation → Finite Model Theory ; Theory of computation → Proof theory ; Theory of computation → Transducers
DOI:
10.4230/LIPIcs.CSL.2025.1
Event:
33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)
Editors:
Jörg Endrullis and Sylvain Schmitz
Series and Publisher:
LIPIcs Logo Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Introduction

The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented at CSL, the annual conference of the EACSL (European Association for Computer Science Logic). This year the 20th Ackermann Award is presented at CSL 2025 in Amsterdam, The Netherlands.

A call for nominations was issued in February 2024, open to any PhD dissertation (on any topic represented at the annual CSL and LICS conferences) formally accepted by a degree-granting institution in fulfilment of the PhD degree between 1 January 2023 and 31 December 2023.

The Jury received ten nominations, which came from a number of different countries around the world: the nominees obtained their doctorates at institutions in Belgium, Canada, Czech Republic, France, Poland and the United Kingdom. The topics covered a wide range of areas in Logic and Computer Science.

This year we received a particularly strong set of nominations. All the nominated PhD theses contained significant contributions to their particular fields. On behalf of the Ackermann Jury, we extend our warmest congratulations to all the nominated candidates for their outstanding work.

All the submissions were evaluated by the Jury, and after two phases of reviewing and extensive discussion, the jury decided to grant the 2024 Ackermann Award jointly to (in alphabetic order):

  • ■

    Gaëtan Douéneau-Tabot for the PhD thesis entitled Optimization of string transducers, completed at University Paris-Cité, France, in 2023;

  • ■

    Aliaume Lopez for the PhD thesis entitled First Order Preservation Theorems in Finite Model Theory: Locality, Topology, and Limit Construction, completed at University Paris-Saclay, France, in 2023.

Citation for Gaëtan Douéneau-Tabot

Gaëtan Douéneau-Tabot shares the 2024 Ackermann Award of the European Association of Computer Science Logic for the PhD thesis

Optimization of string transducers,

which solves open class membership problems for various transducer models, providing effective membership procedures that give rise to program optimization techniques. To achieve this goal, the thesis develops an extensive toolbox for solving class membership problems for transducers, including new characterisations of transducer behaviours.

Background to the thesis

This thesis deals with transducer models, that is, finite automata extended with string outputs, which define functions from strings to strings. String transducers are finite-state devices that represent programs with bounded memory. They are used in language processing tools, compilers, streaming algorithms and model-checkers, amongst others.

Various transducer models have been defined as extensions of the basic model by adding features to increase their expressive power. A natural question then arises: what is the expressive power of each class of transducers? This can be rephrased as a class membership problem: given a transducer with complex features, is there a simpler transducer that has the same behaviour? Such a question can be interpreted as a program optimisation problem: given a program, can we build an equivalent program that requires less resources?

Class membership problems in this context are known to be challenging. In his PhD thesis, Douéneau-Tabot solves multiple instances of the problem, obtaining new results that characterise various classes of transducer models and help understand their relationships.

Contributions of the thesis

The thesis solves open class membership problems for various transducer models. In each case the membership procedure is effective, in the sense that it builds a more efficient transducer whenever one exists, thus providing program optimisation techniques in the setting of transducers. In particular, the techniques can be applied to automatically remove recursion or nested loops for specific classes of programs.

In addition, the thesis provides new computation models and new characterisations that capture pre-existing classes of transductions. These results provide new insights on the expressive power of different kinds of transducers.

The proof techniques introduced are also valuable as a generic toolbox for solving other class membership problems in transducer models, and more generally in automata theory.

Biographical sketch

Gaëtan Douéneau-Tabot carried out his PhD studies at University Paris-Cité, under the supervision of Olivier Carton and Emmanuel Filiot, from 2020 to 2023. During his PhD he (co)-authored papers published in the proceedings of conferences such as ICALP 2023, LICS 2023, FoSSaCS 2023, MFCS 2022, ICALP 2022, MFCS 2021, MFCS 2020. His MFCS 2022 and ICALP 2022 papers won “best student paper” awards.

Citation for Aliaume Lopez

Aliaume Lopez shares the 2024 Ackermann Award of the European Association of Computer Science Logic for the PhD thesis

First Order Preservation Theorems in Finite Model Theory: Locality, Topology, and Limit Constructions,

which presents a systematic approach to investigating preservation theorems in Finite Model Theory, providing tools to explain when and why some classes of structures are well-behaved with respect to preservation theorems. The approach provides a compositional theory for preservation theorems that was previously lacking.

Background to the thesis

Preservation theorems in first-order logic are a collection of results derived from classical model theory, which establish a direct correspondence between the semantic properties of formulas and the constraints imposed on their syntax.

These theorems have a practical impact in computer science, where they can be used for example to characterise syntactic classes of database queries for which the termination and correctness of database algorithms are guaranteed. Unfortunately preservation theorems are notably challenging when focusing on finite models – the models considered in computer science applications. Identifying well-behaved classes has been an active domain of research for the last sixty years, with a series of negative results as well as some positive ones, which motivated the quest for a systematic approach to the problem.

Contributions of the thesis

This thesis presents a systematic approach to investigating preservation theorems within the realm of Finite Model Theory. The traditional ad-hoc proofs are replaced with a theoretical framework that generalises techniques based on locality, and introduces a topological presentation of preservation theorems called logically presented pre-spectral spaces.

Introducing these topological spaces enables the development of a compositional theory for preservation theorems. Additionally, this thesis develops a methodology to systematically examining preservation theorems across inductively defined classes of finite structures, by proving a generic fixed point theorem for a topological restriction of logically presented pre-spectral spaces: Noetherian spaces, which are topological spaces in which every open set is compact.

Biographical sketch

Aliaume Lopez carried out his PhD studies under the supervision of Jean Goubault-Larrecq (École Normale Supérieure Paris-Saclay) and Sylvain Schmitz (University Paris-Cité). The thesis is built around three articles published at CSL 2021, LICS 2022 and FoSSaCS 2023 (he published other papers during his PhD unrelated with the thesis). He is the winner of the E.W. Beth Dissertation Prize 2024. Currently he is a postdoctoral researcher at the University of Warsaw.

Jury

The jury for the Ackermann Award 2024 consisted of nine members, two of them ex officio, namely, the president and the vice-president of EACSL. In addition, the jury also included a representative of SIGLOG (the ACM Special Interest Group on Logic and Computation).

The members of the jury were:

  • ■

    Albert Atserias (Technical University of Catalonia);

  • ■

    Christel Baier (Technical University Dresden);

  • ■

    Andrej Bauer (University of Ljubljana);

  • ■

    Maribel Fernández (King’s College London), president of EACSL;

  • ■

    Joost-Pieter Katoen (RWTH Aachen University), ACM SIGLOG representative;

  • ■

    Delia Kesner (IRIF, University Paris Cité);

  • ■

    Slawomir Lasota (University of Warsaw);

  • ■

    Florin Manea (University of Göttingen), vice-president of EACSL;

  • ■

    Prakash Panangaden (McGill University);

Previous winners

Previous winners of the Ackermann Award were

2005, Oxford:

Mikołaj Bojańczyk from Poland,
Konstantin Korovin from Russia, and
Nathan Segerlind from the USA.

2006, Szeged:

Balder ten Cate from the Netherlands, and
Stefan Milius from Germany.

2007, Lausanne:

Dietmar Berwanger from Germany and Romania,  
Stéphane Lengrand from France, and  
Ting Zhang from the People’s Republic of China.

2008, Bertinoro:

Krishnendu Chatterjee from India.

2009, Coimbra:

Jakob Nordström from Sweden.

2010, Brno:

no award given.

2011, Bergen:

Benjamin Rossman from USA.

2012, Fontainebleau:

Andrew Polonsky from Ukraine, and  
Szymon Toruńczyk from Poland.

2013, Turin:

Matteo Mio from Italy.

2014, Vienna:

Michael Elberfeld from Germany.

2015, Berlin:

Hugo Férée from France, and  
Mickael Randour from Belgium.

2016, Marseille:

Nicolai Kraus from Germany.

2017, Stockholm:

Amaury Pouly from France.

2018, Birmingham:

Amina Doumane from France.

2019, Barcelona (conference in 2020):

Antoine Mottet from France.

2020, Ljubljana (conference online in 2021)

Benjamin Kaminski from Germany.

2021, Göttingen (conference online in 2022)

Marie Fortin from France, and
Sandra Kiefer from Germany.

2022, Warsaw (conference in 2023)

Alexander Bentkamp from The Netherlands.

2023, Naples (conference in 2024)

Gabriele Vanoni from Italy.

Detailed reports on their work appeared in the CSL proceedings and are also available on the EACSL homepage.