26 Search Results for "Meyer, Philipp"

Document
DOI: 10.4230/LIPIcs.SEA.2026.13
Practical Parallel Block Tree Construction

Authors: Robert Clausecker, Florian Kurpicz, and Etienne Palanga

Published in: LIPIcs, Volume 371, 24th International Symposium on Experimental Algorithms (SEA 2026)

Abstract
The block tree [Belazzougui et al., J. Comput. Syst. Sci. '21] is a compressed representation of a length-n text that supports access, rank, and select queries while requiring only O(z log n/z) words of space, where z is the number of Lempel-Ziv factors of the text. In other words, its space requirements are asymptotically comparable to those of the compressed text itself. In practice, block trees offer query performance comparable to that of state-of-the-art compressed rank and select indices. However, their construction is significantly slower, and the fastest known construction algorithms additionally require a significant amount of working memory. To address these limitations, we propose fast and lightweight parallel algorithms for the efficient construction of block trees. Our algorithm achieves similar construction speed than the currently fastest block tree construction algorithm on a single core and is up to eight times faster using 64 cores, while requiring an order of magnitude less memory. Overall, we achieve a speedup of up to 15.5 on 64 cores, which is in line with the parallel construction of the Lempel-Ziv compression.
Cite as

Robert Clausecker, Florian Kurpicz, and Etienne Palanga. Practical Parallel Block Tree Construction. In 24th International Symposium on Experimental Algorithms (SEA 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 371, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{clausecker_et_al:LIPIcs.SEA.2026.13,
  author =	{Clausecker, Robert and Kurpicz, Florian and Palanga, Etienne},
  title =	{{Practical Parallel Block Tree Construction}},
  booktitle =	{24th International Symposium on Experimental Algorithms (SEA 2026)},
  pages =	{13:1--13:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-422-2},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{371},
  editor =	{Aum\"{u}ller, Martin and Finocchi, Irene},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2026.13},
  URN =		{urn:nbn:de:0030-drops-260175},
  doi =		{10.4230/LIPIcs.SEA.2026.13},
  annote =	{Keywords: block tree, shared memory, compression, SIMD, Karp-Rabin fingerprints}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2026.44
Tilt Automata: Gathering Particles with Uniform External Control

Authors: Sándor P. Fekete, Jonas Friemel, Peter Kramer, Jan-Marc Reinhardt, Christian Rieck, and Christian Scheffer

Published in: LIPIcs, Volume 367, 42nd International Symposium on Computational Geometry (SoCG 2026)

Abstract
Motivated by targeted drug delivery, we investigate the gathering of particles in the full tilt model of externally controlled motion planning: A set of particles is located at the tiles of a polyomino with all particles reacting uniformly to an external force by moving as far as possible in one of the four axis-parallel directions until they hit the boundary. The goal is to choose a sequence of directions that moves all particles to a common position. Our results include a polynomial-time algorithm for gathering in a completely filled polyomino as well as hardness reductions for approximating shortest gathering sequences and for determining whether the particles in a partially filled polyomino can be gathered. We pay special attention to the impact of restricted geometry, particularly polyominoes without holes. As a corollary, we make progress on an open question from [Balanza-Martinez et al., SODA 2020] by showing that deciding whether a given position can be occupied remains NP-hard in polyominoes without holes. Our results build on a connection we establish between tilt models and the theory of synchronizing automata.
Cite as

Sándor P. Fekete, Jonas Friemel, Peter Kramer, Jan-Marc Reinhardt, Christian Rieck, and Christian Scheffer. Tilt Automata: Gathering Particles with Uniform External Control. In 42nd International Symposium on Computational Geometry (SoCG 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 367, pp. 44:1-44:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fekete_et_al:LIPIcs.SoCG.2026.44,
  author =	{Fekete, S\'{a}ndor P. and Friemel, Jonas and Kramer, Peter and Reinhardt, Jan-Marc and Rieck, Christian and Scheffer, Christian},
  title =	{{Tilt Automata: Gathering Particles with Uniform External Control}},
  booktitle =	{42nd International Symposium on Computational Geometry (SoCG 2026)},
  pages =	{44:1--44:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-418-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{367},
  editor =	{Ahn, Hee-Kap and Hoffmann, Michael and Nayyeri, Amir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2026.44},
  URN =		{urn:nbn:de:0030-drops-258508},
  doi =		{10.4230/LIPIcs.SoCG.2026.44},
  annote =	{Keywords: Uniform control, gathering, full tilt, polyominoes, synchronizing automata}
}
Document
DOI: 10.4230/OASIcs.PARMA-DITAM.2026.2
SLURM-Managed HyperParameter Optimization

Authors: Anusha Chattopadhyay, Hendrik Borras, Bernhard Klein, and Holger Fröning

Published in: OASIcs, Volume 141, 17th Workshop on Parallel Programming and Run-Time Management Techniques for Many-Core Architectures and 15th Workshop on Design Tools and Architectures for Multicore Embedded Computing Platforms (PARMA-DITAM 2026)

Abstract
Hyperparameter optimization (HPO) is essential for achieving state-of-the-art performance in machine learning, yet it is computationally demanding, particularly on shared or resource-constrained clusters. We present a system that integrates the Asynchronous Successive Halving Algorithm (ASHA) with SEML, the SLURM Experiment Management Library - an experiment orchestration layer that provides declarative configuration, provenance, metric tracking, and robust SLURM job management. The resulting open-source tool enables scalable, fault-tolerant HPO on SLURM-managed infrastructure: SEML handles experiment specification, versioning, and scheduling, while ASHA performs asynchronous early stopping and resource reallocation to concentrate computation on promising configurations. Overall, the system streamlines experiment lifecycle management, enables distributed evaluations with minimal manual effort, and reduces the time required to reach high-quality configurations compared to conventional Grid and Random Search methods under similar compute budgets.
Cite as

Anusha Chattopadhyay, Hendrik Borras, Bernhard Klein, and Holger Fröning. SLURM-Managed HyperParameter Optimization. In 17th Workshop on Parallel Programming and Run-Time Management Techniques for Many-Core Architectures and 15th Workshop on Design Tools and Architectures for Multicore Embedded Computing Platforms (PARMA-DITAM 2026). Open Access Series in Informatics (OASIcs), Volume 141, pp. 2:1-2:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{chattopadhyay_et_al:OASIcs.PARMA-DITAM.2026.2,
  author =	{Chattopadhyay, Anusha and Borras, Hendrik and Klein, Bernhard and Fr\"{o}ning, Holger},
  title =	{{SLURM-Managed HyperParameter Optimization}},
  booktitle =	{17th Workshop on Parallel Programming and Run-Time Management Techniques for Many-Core Architectures and 15th Workshop on Design Tools and Architectures for Multicore Embedded Computing Platforms (PARMA-DITAM 2026)},
  pages =	{2:1--2:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-416-1},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{141},
  editor =	{Baroffio, Davide and Busia, Paola and Denisov, Lev and Shukla, Nitin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.PARMA-DITAM.2026.2},
  URN =		{urn:nbn:de:0030-drops-256697},
  doi =		{10.4230/OASIcs.PARMA-DITAM.2026.2},
  annote =	{Keywords: Hyperparameter optimization, Asynchronous Successive Halving Algorithm (ASHA), Experiment management, SLURM, SEML, Open Source}
}
Document
DOI: 10.4230/OASIcs.NINeS.2026.4
Understanding Partial Reachability in the Internet Core

Authors: Guillermo Baltra, Tarang Saluja, Yuri Pradkin, and John Heidemann

Published in: OASIcs, Volume 139, 1st New Ideas in Networked Systems (NINeS 2026)

Abstract
Routing strives to connect all the Internet, but compete: political pressure threatens routing fragmentation; architectural changes such as private clouds, carrier-grade NAT, and firewalls make connectivity conditional; and commercial disputes create partial reachability for days or years. This paper suggests persistent, partial reachability is fundamental to the Internet and an underexplored problem. We first derive a conceptual definition of the Internet core based on connectivity, not authority. We identify peninsulas: persistent, partial connectivity; and islands: when computers are partitioned from the Internet core. Second, we develop algorithms to observe each across the Internet, and apply them to two existing measurement systems: Trinocular, where 6 locations observe 5M networks frequently, and RIPE Atlas, where 13k locations scan the DNS roots frequently. Cross-validation shows our findings are stable over three years of data, and consistent with as few as 3 geographically-distributed observers. We validate peninsulas and islands against CAIDA Ark, showing good recall (0.94) and bounding precision between 0.42 and 0.82. Finally, our work has broad practical impact: we show that peninsulas are more common than Internet outages. Factoring out peninsulas and islands as noise can improve existing measurement systems; their "noise" is 5× to 9.7× larger than the operational events in RIPE’s DNSmon. We show that most peninsula events are routing transients (45%), but most peninsula-time (90%) is due to a few (7%) long-lived events. Our work helps inform Internet policy and governance, with our neutral definition showing no single country or organization can unilaterally control the Internet core.
Cite as

Guillermo Baltra, Tarang Saluja, Yuri Pradkin, and John Heidemann. Understanding Partial Reachability in the Internet Core. In 1st New Ideas in Networked Systems (NINeS 2026). Open Access Series in Informatics (OASIcs), Volume 139, pp. 4:1-4:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{baltra_et_al:OASIcs.NINeS.2026.4,
  author =	{Baltra, Guillermo and Saluja, Tarang and Pradkin, Yuri and Heidemann, John},
  title =	{{Understanding Partial Reachability in the Internet Core}},
  booktitle =	{1st New Ideas in Networked Systems (NINeS 2026)},
  pages =	{4:1--4:32},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-414-7},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{139},
  editor =	{Argyraki, Katerina and Panda, Aurojit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.NINeS.2026.4},
  URN =		{urn:nbn:de:0030-drops-255892},
  doi =		{10.4230/OASIcs.NINeS.2026.4},
  annote =	{Keywords: Internet, Internet reliability, Network outages, Active measurements}
}
Document
DOI: 10.4230/LIPIcs.STACS.2026.10
A Polynomial Bound on the Pathwidth of Graphs Edge-Coverable by k Shortest Paths

Authors: Julien Baste, Lucas De Meyer, Ugo Giocanti, Etienne Objois, and Timothé Picavet

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
Dumas, Foucaud, Perez and Todinca [SIAM J. Disc. Math., 2024] recently proved that every graph whose edge set can be covered by k shortest paths has pathwidth at most 3^k. In this paper, we improve this upper bound on the pathwidth to a polynomial bound; namely, we show that every graph whose edge set can be covered by k shortest paths has pathwidth O(k⁴), answering a question from the same paper. Moreover, we also prove that when k ≤ 3, every such graph has pathwidth at most k (and this bound is tight). Eventually, we show that even though there exist graphs with arbitrary large treewidth whose vertex set can be covered by 2 isometric trees, every graph whose set of edges can be covered by 2 isometric trees has treewidth at most 2.
Cite as

Julien Baste, Lucas De Meyer, Ugo Giocanti, Etienne Objois, and Timothé Picavet. A Polynomial Bound on the Pathwidth of Graphs Edge-Coverable by k Shortest Paths. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{baste_et_al:LIPIcs.STACS.2026.10,
  author =	{Baste, Julien and De Meyer, Lucas and Giocanti, Ugo and Objois, Etienne and Picavet, Timoth\'{e}},
  title =	{{A Polynomial Bound on the Pathwidth of Graphs Edge-Coverable by k Shortest Paths}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{10:1--10:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.10},
  URN =		{urn:nbn:de:0030-drops-254999},
  doi =		{10.4230/LIPIcs.STACS.2026.10},
  annote =	{Keywords: Structural Graph Theory, Coverings, Metrics, Pathwidth, Treewdidth, Parameterized Algorithms, Layerings}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.8
Register-Bounded Synthesis from Constraint LTL

Authors: Nino Dauvier, Emmanuel Filiot, and Pierre-Alain Reynier

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We consider synthesis problems from logical specifications over infinite data domains, expressed in the logic constraint LTL (CLTL), which extends LTL with predicates over an infinite set of data values. We consider register-bounded synthesis, where the goal is to automatically generate, if it exists, a transducer with r registers that realizes a given CLTL formula, where r is also given as input. We prove that CLTL register-bounded synthesis is 2ExpTime-c for various data domains such as any infinite set with equality, (ℚ, <), and (ℕ, <). For the latter domain, this contrasts with known undecidability results of (unbounded) register CLTL synthesis, by Bhaskar and Praveen. Lastly, we consider synthesis in a partial observation setting by extending CLTL with invisible variables.
Cite as

Nino Dauvier, Emmanuel Filiot, and Pierre-Alain Reynier. Register-Bounded Synthesis from Constraint LTL. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{dauvier_et_al:LIPIcs.CSL.2026.8,
  author =	{Dauvier, Nino and Filiot, Emmanuel and Reynier, Pierre-Alain},
  title =	{{Register-Bounded Synthesis from Constraint LTL}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.8},
  URN =		{urn:nbn:de:0030-drops-254322},
  doi =		{10.4230/LIPIcs.CSL.2026.8},
  annote =	{Keywords: Synthesis, Data words, Constraint linear time logic, Register transducer}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.22
On the Algorithmic Structure of Dialectica Realisers

Authors: Davide Barbarossa and Thomas Powell

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Gödel’s Dialectica interpretation is a fundamental tool for the extraction of computational content from proofs, and plays a central role in today’s proof mining program. In the past decades, it has also been studied from the perspective of programming languages, and our contribution is in that direction. Specifically, we present Dialectica as a collection of rules in the style of Hoare logic, where Dialectica is now viewed as a language for specifying procedural programs that come with a forward and backward direction. This viewpoint captures the interesting dynamics of realisers extracted by the Dialectica interpretation, and we illustrate this by defining a generalised backpropagation semantics for a fragment of this language. We envisage this work as providing a base for several future developments, both theoretical and practical, which we outline at the end.
Cite as

Davide Barbarossa and Thomas Powell. On the Algorithmic Structure of Dialectica Realisers. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{barbarossa_et_al:LIPIcs.CSL.2026.22,
  author =	{Barbarossa, Davide and Powell, Thomas},
  title =	{{On the Algorithmic Structure of Dialectica Realisers}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{22:1--22:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.22},
  URN =		{urn:nbn:de:0030-drops-254466},
  doi =		{10.4230/LIPIcs.CSL.2026.22},
  annote =	{Keywords: Dialectica interpretation, Hoare logic, Programs from proofs}
}
Document
DOI: 10.4230/DagMan.11.1.19
Conversational Agents: A Framework for Evaluation (CAFE) (Dagstuhl Perspectives Workshop 24352)

Authors: Christine Bauer, Li Chen, Nicola Ferro, Norbert Fuhr, Avishek Anand, Timo Breuer, Guglielmo Faggioli, Ophir Frieder, Hideo Joho, Jussi Karlgren, Johannes Kiesel, Bart P. Knijnenburg, Aldo Lipani, Lien Michiels, Andrea Papenmeier, Maria Soledad Pera, Mark Sanderson, Scott Sanner, Benno Stein, Johanne R. Trippas, Karin Verspoor, and Martijn C. Willemsen

Published in: Dagstuhl Manifestos, Volume 11, Issue 1 (2025)

Abstract
During the workshop, we deeply discussed what CONversational Information ACcess (CONIAC) is and its unique features, proposing a world model abstracting it, and defined the Conversational Agents Framework for Evaluation (CAFE) for the evaluation of CONIAC systems, consisting of six major components: 1) goals of the system’s stakeholders, 2) user tasks to be studied in the evaluation, 3) aspects of the users carrying out the tasks, 4) evaluation criteria to be considered, 5) evaluation methodology to be applied, and 6) measures for the quantitative criteria chosen.
Cite as

Christine Bauer, Li Chen, Nicola Ferro, Norbert Fuhr, Avishek Anand, Timo Breuer, Guglielmo Faggioli, Ophir Frieder, Hideo Joho, Jussi Karlgren, Johannes Kiesel, Bart P. Knijnenburg, Aldo Lipani, Lien Michiels, Andrea Papenmeier, Maria Soledad Pera, Mark Sanderson, Scott Sanner, Benno Stein, Johanne R. Trippas, Karin Verspoor, and Martijn C. Willemsen. Conversational Agents: A Framework for Evaluation (CAFE) (Dagstuhl Perspectives Workshop 24352). In Dagstuhl Manifestos, Volume 11, Issue 1, pp. 19-67, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{bauer_et_al:DagMan.11.1.19,
  author =	{Bauer, Christine and Chen, Li and Ferro, Nicola and Fuhr, Norbert and Anand, Avishek and Breuer, Timo and Faggioli, Guglielmo and Frieder, Ophir and Joho, Hideo and Karlgren, Jussi and Kiesel, Johannes and Knijnenburg, Bart P. and Lipani, Aldo and Michiels, Lien and Papenmeier, Andrea and Pera, Maria Soledad and Sanderson, Mark and Sanner, Scott and Stein, Benno and Trippas, Johanne R. and Verspoor, Karin and Willemsen, Martijn C.},
  title =	{{Conversational Agents: A Framework for Evaluation (CAFE) (Dagstuhl Perspectives Workshop 24352)}},
  pages =	{19--67},
  journal =	{Dagstuhl Manifestos},
  ISSN =	{2193-2433},
  year =	{2025},
  volume =	{11},
  number =	{1},
  editor =	{Bauer, Christine and Chen, Li and Ferro, Nicola and Fuhr, Norbert and Anand, Avishek and Breuer, Timo and Faggioli, Guglielmo and Frieder, Ophir and Joho, Hideo and Karlgren, Jussi and Kiesel, Johannes and Knijnenburg, Bart P. and Lipani, Aldo and Michiels, Lien and Papenmeier, Andrea and Pera, Maria Soledad and Sanderson, Mark and Sanner, Scott and Stein, Benno and Trippas, Johanne R. and Verspoor, Karin and Willemsen, Martijn C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagMan.11.1.19},
  URN =		{urn:nbn:de:0030-drops-252722},
  doi =		{10.4230/DagMan.11.1.19},
  annote =	{Keywords: Conversational Agents, Evaluation, Information Access}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2025.24
A Note on the Parameterised Complexity of Coverability in Vector Addition Systems

Authors: Michał Pilipczuk, Sylvain Schmitz, and Henry Sinclair-Banks

Published in: LIPIcs, Volume 358, 20th International Symposium on Parameterized and Exact Computation (IPEC 2025)

Abstract
We investigate the parameterised complexity of the classic coverability problem for vector addition systems (VAS): V ⊆ ℤ^d, an initial configuration s ∈ ℕ^d, and a target configuration t ∈ ℕ^d, decide whether starting from s, one can iteratively add vectors from V to ultimately arrive at a configuration that is larger than or equal to t on every coordinate, while not observing any negative value on any coordinate along the way. We consider two natural parameters for the problem: the dimension d and the size of V, defined as the total bitsize of its encoding. We present several results charting the complexity of those two parameterisations, among which the highlight is that coverability for VAS parameterised by the dimension and with all the numbers in the input encoded in unary is complete for the class XNL under PL-reductions. We also discuss open problems in the topic, most notably the question about fixed-parameter tractability for the parameterisation by the size of V.
Cite as

Michał Pilipczuk, Sylvain Schmitz, and Henry Sinclair-Banks. A Note on the Parameterised Complexity of Coverability in Vector Addition Systems. In 20th International Symposium on Parameterized and Exact Computation (IPEC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 358, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{pilipczuk_et_al:LIPIcs.IPEC.2025.24,
  author =	{Pilipczuk, Micha{\l} and Schmitz, Sylvain and Sinclair-Banks, Henry},
  title =	{{A Note on the Parameterised Complexity of Coverability in Vector Addition Systems}},
  booktitle =	{20th International Symposium on Parameterized and Exact Computation (IPEC 2025)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-407-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{358},
  editor =	{Agrawal, Akanksha and van Leeuwen, Erik Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2025.24},
  URN =		{urn:nbn:de:0030-drops-251563},
  doi =		{10.4230/LIPIcs.IPEC.2025.24},
  annote =	{Keywords: vector addition system, Petri net, parameterised complexity, coverability}
}
Document
DOI: 10.4230/LIPIcs.DISC.2025.37
Towards Optimal Distributed Edge Coloring with Fewer Colors

Authors: Manuel Jakob, Yannic Maus, and Florian Schager

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
There is a huge difference in techniques and runtimes of distributed algorithms for problems that can be solved by a sequential greedy algorithm and those that cannot. A prime example of this contrast appears in the edge coloring problem: while (2Δ-1)-edge coloring - where Δ is the maximum degree - can be solved in 𝒪(log^{∗}(n)) rounds on constant-degree graphs, the seemingly minor reduction to (2Δ-2) colors leads to an Ω(log n) lower bound [Chang, He, Li, Pettie & Uitto, SODA'18]. Understanding this sharp divide between very local problems and inherently more global ones remains a central open question in distributed computing and it is a core focus of this paper. As our main contribution we design a deterministic distributed 𝒪(log n)-round reduction from the (2Δ-2)-edge coloring problem to the much easier (2Δ-1)-edge coloring problem. This reduction is optimal, as the (2Δ-2)-edge coloring problem admits an Ω(log n) lower bound that even holds on the class of constant-degree graphs, whereas the 2Δ-1-edge coloring problem can be solved in 𝒪(log^{∗}n) rounds. By plugging in the (2Δ-1)-edge coloring algorithms from [Balliu, Brandt, Kuhn & Olivetti, PODC'22] running in 𝒪(log^{12}Δ + log^{∗} n) rounds, we obtain an optimal runtime of 𝒪(log n) rounds as long as Δ = 2^{𝒪(log^{1/12} n)}. Previously, such an optimal algorithm was only known for the class of constant-degree graphs [Brandt, Maus, Narayanan, Schager & Uitto, SODA'25]. Furthermore, on general graphs our reduction improves the runtime from 𝒪̃(log³ n) to 𝒪̃(log^{5/3} n). In addition, we also obtain an optimal 𝒪(log log n)-round randomized reduction of (2Δ - 2)-edge coloring to (2Δ - 1)-edge coloring. This leads to a 𝒪̃(log^{5/3} log n)-round (2Δ-2)-edge coloring algorithm, which beats the (very recent) previous state-of-the-art taking 𝒪̃(log^{8/3}log n) rounds from [Bourreau, Brandt & Nolin, STOC'25]. Lastly, we obtain an 𝒪(log_Δ n)-round reduction from the (2Δ-1)-edge coloring, albeit to the somewhat harder maximal independent set (MIS) problem.
Cite as

Manuel Jakob, Yannic Maus, and Florian Schager. Towards Optimal Distributed Edge Coloring with Fewer Colors. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 37:1-37:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jakob_et_al:LIPIcs.DISC.2025.37,
  author =	{Jakob, Manuel and Maus, Yannic and Schager, Florian},
  title =	{{Towards Optimal Distributed Edge Coloring with Fewer Colors}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{37:1--37:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.37},
  URN =		{urn:nbn:de:0030-drops-248547},
  doi =		{10.4230/LIPIcs.DISC.2025.37},
  annote =	{Keywords: distributed graph algorithms, edge coloring, LOCAL model}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2025.37
LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper)

Authors: Eric Vin, Kyle A. Miller, and Daniel J. Fremont

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We propose LeanLTL, a unifying framework for linear temporal logics in Lean 4. LeanLTL supports reasoning about traces that represent either infinite or finite linear time. The library allows traditional LTL syntax to be combined with arbitrary Lean expressions, making it straightforward to define properties involving numerical or other types. We prove that standard flavors of LTL can be embedded in our framework. The library also provides automation for reasoning about LeanLTL formulas in a way that facilitates using Lean’s existing tactics. Finally, we provide examples illustrating the utility of the library in reasoning about systems that come from applications.
Cite as

Eric Vin, Kyle A. Miller, and Daniel J. Fremont. LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper). In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 37:1-37:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vin_et_al:LIPIcs.ITP.2025.37,
  author =	{Vin, Eric and Miller, Kyle A. and Fremont, Daniel J.},
  title =	{{LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{37:1--37:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.37},
  URN =		{urn:nbn:de:0030-drops-246356},
  doi =		{10.4230/LIPIcs.ITP.2025.37},
  annote =	{Keywords: Linear Temporal Logic, Interactive Theorem Proving, Lean 4}
}
Document
DOI: 10.4230/OASIcs.Programming.2025.10
Shica - Improving the Programming Experience for Agent-Based, Distributed, Physical Computing Systems

Authors: Hiroto Shikada and Ian Piumarta

Published in: OASIcs, Volume 134, Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)

Abstract
Agent-based and distributed computing systems play an important role in many fields. Programming these systems can be annoying because of the complexity of managing multiple asynchronous processes and state transitions, sometimes hidden inter-dependencies between program elements, and (often) unnecessarily terse, un-intuitive syntax. In this paper we describe the design and implementation of Shica, an experimental language designed for physical computing that is fun to program. Shica unifies state-based, event-based, and distributed programming along with some elements of context-oriented. We informally evaluate Shica’s characteristics including its suitability for deployment on resource-constrained, embedded devices and its contribution to improving the quality of the programming experience by maximizing scope, economy, and elegance of expression.
Cite as

Hiroto Shikada and Ian Piumarta. Shica - Improving the Programming Experience for Agent-Based, Distributed, Physical Computing Systems. In Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025). Open Access Series in Informatics (OASIcs), Volume 134, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{shikada_et_al:OASIcs.Programming.2025.10,
  author =	{Shikada, Hiroto and Piumarta, Ian},
  title =	{{Shica - Improving the Programming Experience for Agent-Based, Distributed, Physical Computing Systems}},
  booktitle =	{Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)},
  pages =	{10:1--10:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-382-9},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{134},
  editor =	{Edwards, Jonathan and Perera, Roly and Petricek, Tomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Programming.2025.10},
  URN =		{urn:nbn:de:0030-drops-242948},
  doi =		{10.4230/OASIcs.Programming.2025.10},
  annote =	{Keywords: Programming Languages, run-time Systems, agent-based Programming}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.38
The Complexity of Separability for Semilinear Sets and Parikh Automata

Authors: Elias Rojas Collins, Chris Köcher, and Georg Zetzsche

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
In a separability problem, we are given two sets K and L from a class 𝒞, and we want to decide whether there exists a set S from a class 𝒮 such that K ⊆ S and S ∩ L = ∅. In this case, we speak of separability of sets in 𝒞 by sets in 𝒮. We study two types of separability problems. First, we consider separability of semilinear sets (i.e. subsets of ℕ^d for some d) by sets definable by quantifier-free monadic Presburger formulas (or equivalently, the recognizable subsets of ℕ^d). Here, a formula is monadic if each atom uses at most one variable. Second, we consider separability of languages of Parikh automata by regular languages. A Parikh automaton is a machine with access to counters that can only be incremented, and have to meet a semilinear constraint at the end of the run. Both of these separability problems are known to be decidable with elementary complexity. Our main results are that both problems are coNP-complete. In the case of semilinear sets, coNP-completeness holds regardless of whether the input sets are specified by existential Presburger formulas, quantifier-free formulas, or semilinear representations. Our results imply that recognizable separability of rational subsets of Σ* × ℕ^d (shown decidable by Choffrut and Grigorieff) is coNP-complete as well. Another application is that regularity of deterministic Parikh automata (where the target set is specified using a quantifier-free Presburger formula) is coNP-complete as well.
Cite as

Elias Rojas Collins, Chris Köcher, and Georg Zetzsche. The Complexity of Separability for Semilinear Sets and Parikh Automata. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{collins_et_al:LIPIcs.MFCS.2025.38,
  author =	{Collins, Elias Rojas and K\"{o}cher, Chris and Zetzsche, Georg},
  title =	{{The Complexity of Separability for Semilinear Sets and Parikh Automata}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{38:1--38:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.38},
  URN =		{urn:nbn:de:0030-drops-241457},
  doi =		{10.4230/LIPIcs.MFCS.2025.38},
  annote =	{Keywords: Vector Addition System, Separability, Regular Language}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2025.14
Pareto Fronts for Compositionally Solving String Diagrams of Parity Games

Authors: Kazuki Watanabe

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
Open parity games are proposed as a compositional extension of parity games with algebraic operations, forming string diagrams of parity games. A potential application of string diagrams of parity games is to describe a large parity game with a given compositional structure and solve it efficiently as a divide-and-conquer algorithm by exploiting its compositional structure. Building on our recent progress in open Markov decision processes, we introduce Pareto fronts of open parity games, offering a framework for multi-objective solutions. We establish the positional determinacy of open parity games with respect to their Pareto fronts through a novel translation method. Our translation converts an open parity game into a parity game tailored to a given single-objective. Furthermore, we present a simple algorithm for solving open parity games, derived from this translation that allows the application of existing efficient algorithms for parity games. Expanding on this foundation, we develop a compositional algorithm for string diagrams of parity games.
Cite as

Kazuki Watanabe. Pareto Fronts for Compositionally Solving String Diagrams of Parity Games. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{watanabe:LIPIcs.CALCO.2025.14,
  author =	{Watanabe, Kazuki},
  title =	{{Pareto Fronts for Compositionally Solving String Diagrams of Parity Games}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.14},
  URN =		{urn:nbn:de:0030-drops-235734},
  doi =		{10.4230/LIPIcs.CALCO.2025.14},
  annote =	{Keywords: parity game, compositionality, string diagram}
}
Document
Experience Paper
DOI: 10.4230/LIPIcs.ECOOP.2025.37
RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper)

Authors: Tomáš Dacík and Tomáš Vojnar

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
We present RacerF, a novel static analyser for thread-modular data race detection. The approach behind RacerF exploits static analysis of sequential program behaviour whose results are generalised for multi-threaded programs using a combination of lightweight under- and over-approximating methods. The tool is implemented as a plugin of the Frama-C platform and can leverage several analysis backends, most notably the Frama-C’s abstract interpreter EVA. Although our methods are mostly heuristic without providing formal guarantees, our experimental evaluation shows that even for intricate programs, RacerF can provide very precise results competitive with more heavyweight approaches while being faster than them.
Cite as

Tomáš Dacík and Tomáš Vojnar. RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dacik_et_al:LIPIcs.ECOOP.2025.37,
  author =	{Dac{\'\i}k, Tom\'{a}\v{s} and Vojnar, Tom\'{a}\v{s}},
  title =	{{RacerF: Lightweight Static Data Race Detection for C Code}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{37:1--37:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.37},
  URN =		{urn:nbn:de:0030-drops-233298},
  doi =		{10.4230/LIPIcs.ECOOP.2025.37},
  annote =	{Keywords: concurrency, data race detection, static analysis}
}
  • Refine by Type
  • 26 Document/PDF
  • 21 Document/HTML

  • Refine by Publication Year
  • 7 2026
  • 12 2025
  • 1 2024
  • 2 2023
  • 1 2022
  • Show More...

  • Refine by Author
  • 2 Maus, Yannic
  • 1 Ahmed, Rehan
  • 1 Anand, Avishek
  • 1 Ayoubi, Kamran
  • 1 Baguley, Samuel
  • Show More...

  • Refine by Series/Journal
  • 17 LIPIcs
  • 3 OASIcs
  • 2 LITES
  • 2 TGDK
  • 1 DagMan
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Automata over infinite objects
  • 2 Theory of computation → Distributed computing models
  • 2 Theory of computation → Modal and temporal logics
  • 2 Theory of computation → Parameterized complexity and exact algorithms
  • 1 Computer systems organization → Single instruction, multiple data
  • Show More...

  • Refine by Keyword
  • 1 AI
  • 1 Accountability
  • 1 Active measurements
  • 1 Asynchronous Successive Halving Algorithm (ASHA)
  • 1 Automata over infinite words
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact