DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2026.27

Polymorphism Meets DHOL

Authors: Rhea Ranalter, Florian Rabe, and Cezary Kaliszyk

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract

DHOL is an extensional, classical logic that equips the well-known higher-order logic (HOL) with dependent types. This allows for concise encodings of important domains like size-bounded data structures, category theory, or proof theory. Automation support is obtained by translating DHOL to HOL, for which powerful modern automated theorem provers are available. However, a critically missing feature of DHOL is polymorphism. We develop the syntax and semantics of polymorphic DHOL and extend the translation accordingly. We implement the translation in the logic-embedding tool and evaluate it on a range of TPTP formalizations. The logic-embedding tool, together with an off-the-shelf HOL theorem prover easily creates a PDHOL theorem prover for experimenting.

Cite as

Rhea Ranalter, Florian Rabe, and Cezary Kaliszyk. Polymorphism Meets DHOL. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 27:1-27:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ranalter_et_al:LIPIcs.FSCD.2026.27,
  author =	{Ranalter, Rhea and Rabe, Florian and Kaliszyk, Cezary},
  title =	{{Polymorphism Meets DHOL}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{27:1--27:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.27},
  URN =		{urn:nbn:de:0030-drops-263774},
  doi =		{10.4230/LIPIcs.FSCD.2026.27},
  annote =	{Keywords: Polymorphism, Dependent Types, Higher-order Logic, Automated Reasoning}
}

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.SWAT.2026.20

Near-Linear and Parameterized Approximations for Maximum Cliques in Disk Graphs

Authors: Jie Gao, Paweł Gawrychowski, Panos Giannopoulos, Wolfgang Mulzer, Satyam Singh, Frank Staals, and Meirav Zehavi

Published in: LIPIcs, Volume 370, 20th Scandinavian Symposium on Algorithm Theory (SWAT 2026)

Abstract

A disk graph is the intersection graph of (closed) disks in the plane. We consider the classic problem of finding a maximum clique in a disk graph. For general disk graphs, the complexity of this problem is still open, but for unit disk graphs, it is well known to be in P. The currently fastest algorithm runs in time O(n^{7/3+ o(1)}), where n denotes the number of disks [Jared Espenant et al., 2023; J. Mark Keil and Debajyoti Mondal, 2025]. Moreover, for the case of disk graphs with t distinct radii, the problem has also recently been shown to be in XP. More specifically, it is solvable in time O^*(n^{2t}) [J. Mark Keil and Debajyoti Mondal, 2025]. In this paper, we present algorithms with improved running times by allowing for approximate solutions and by using randomization: [(i)] 1) for unit disk graphs, we give an algorithm that, with constant success probability, computes a (1-ε)-approximate maximum clique in expected time Õ(n/ε²); and 2) for disk graphs with t distinct radii, we give a parameterized approximation scheme that, with a constant success probability, computes a (1-ε)-approximate maximum clique in expected time Õ(f(t)⋅ (1/ε)^{O(t)} ⋅ n), for some (exponential) function f(t).

Cite as

Jie Gao, Paweł Gawrychowski, Panos Giannopoulos, Wolfgang Mulzer, Satyam Singh, Frank Staals, and Meirav Zehavi. Near-Linear and Parameterized Approximations for Maximum Cliques in Disk Graphs. In 20th Scandinavian Symposium on Algorithm Theory (SWAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 370, pp. 20:1-20:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{gao_et_al:LIPIcs.SWAT.2026.20,
  author =	{Gao, Jie and Gawrychowski, Pawe{\l} and Giannopoulos, Panos and Mulzer, Wolfgang and Singh, Satyam and Staals, Frank and Zehavi, Meirav},
  title =	{{Near-Linear and Parameterized Approximations for Maximum Cliques in Disk Graphs}},
  booktitle =	{20th Scandinavian Symposium on Algorithm Theory (SWAT 2026)},
  pages =	{20:1--20:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-421-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{370},
  editor =	{Fraigniaud, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SWAT.2026.20},
  URN =		{urn:nbn:de:0030-drops-260563},
  doi =		{10.4230/LIPIcs.SWAT.2026.20},
  annote =	{Keywords: Maximum Clique, Disk Graphs, Unit Disk Graphs, FPT Approximation}
}

Document

DOI: 10.4230/LIPIcs.SWAT.2026.25

Parameterized Critical Node Cut Revisited

Authors: Dušan Knop, Nikolaos Melissinos, and Manolis Vasilakis

Published in: LIPIcs, Volume 370, 20th Scandinavian Symposium on Algorithm Theory (SWAT 2026)

Abstract

We study how to sparsify connectivity in graphs under a tight deletion budget. Given a graph G and integers k,x ≥ 0, Critical Node Cut (CNC) asks whether we can delete at most k vertices so that the number of remaining unordered pairs of connected vertices is at most x. CNC generalizes Vertex Cover (the case x = 0) and models tasks in network design, epidemiology, and social network analysis. We comprehensively map the structural parameterized complexity landscape for Critical Node Cut. First, we prove W[1]-hardness for the combined parameter k + fes + Δ + pw, where fes is the feedback edge set number, Δ the maximum degree, and pw the pathwidth of the input graph, respectively. This significantly improves over the known W[1]-hardness for k+tw, where tw denotes the treewidth, and is tight in that tree-depth together with maximum degree trivially yields FPT. Second, we give new positive results. Specifically, we identify three structural parameters-max-leaf number, vertex integrity, and modular-width-that render the problem fixed-parameter tractable, and develop a polynomial-time algorithm for graphs of constant clique-width. Third, leveraging a technique introduced by Lampis [ICALP '14], we develop an FPT approximation scheme that, for any ε > 0, computes a (1+ε)-approximate solution in time (tw / ε)^{𝒪(tw)} n^{𝒪(1)}. Finally, we show that CNC admits no polynomial kernel when parameterized by vertex cover number, unless standard assumptions fail. Together, these results substantially sharpen the known complexity landscape for CNC.

Cite as

Dušan Knop, Nikolaos Melissinos, and Manolis Vasilakis. Parameterized Critical Node Cut Revisited. In 20th Scandinavian Symposium on Algorithm Theory (SWAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 370, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{knop_et_al:LIPIcs.SWAT.2026.25,
  author =	{Knop, Du\v{s}an and Melissinos, Nikolaos and Vasilakis, Manolis},
  title =	{{Parameterized Critical Node Cut Revisited}},
  booktitle =	{20th Scandinavian Symposium on Algorithm Theory (SWAT 2026)},
  pages =	{25:1--25:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-421-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{370},
  editor =	{Fraigniaud, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SWAT.2026.25},
  URN =		{urn:nbn:de:0030-drops-260617},
  doi =		{10.4230/LIPIcs.SWAT.2026.25},
  annote =	{Keywords: Critical Node Cut, Parameterized Complexity, Treewidth}
}

Document

DOI: 10.4230/LIPIcs.SoCG.2026.63

Unavoidable Patterns and Plane Paths in Dense Topological Graphs

Authors: Balázs Keszegh, Andrew Suk, Gábor Tardos, and Ji Zeng

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

Abstract

Let C_{s,t} be the complete bipartite geometric graph, with s and t vertices on two distinct parallel lines respectively, and all s t straight-line edges drawn between them. In this paper, we show that every complete bipartite simple topological graph, with parts of size 2(k-1)⁴ + 1 and 2^{k^{5k}}, contains a topological subgraph weakly isomorphic to C_{k,k}. As a corollary, every n-vertex simple topological graph not containing a plane path of length k has at most O_k(n^{2 - 8/k⁴}) edges. When k = 3, we obtain a stronger bound by showing that every n-vertex simple topological graph not containing a plane path of length 3 has at most O(n^{4/3}) edges. We also prove that x-monotone simple topological graphs not containing a plane path of length 3 have at most a linear number of edges.

Cite as

Balázs Keszegh, Andrew Suk, Gábor Tardos, and Ji Zeng. Unavoidable Patterns and Plane Paths in Dense Topological Graphs. In 42nd International Symposium on Computational Geometry (SoCG 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 367, pp. 63:1-63:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{keszegh_et_al:LIPIcs.SoCG.2026.63,
  author =	{Keszegh, Bal\'{a}zs and Suk, Andrew and Tardos, G\'{a}bor and Zeng, Ji},
  title =	{{Unavoidable Patterns and Plane Paths in Dense Topological Graphs}},
  booktitle =	{42nd International Symposium on Computational Geometry (SoCG 2026)},
  pages =	{63:1--63:15},
  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.63},
  URN =		{urn:nbn:de:0030-drops-258706},
  doi =		{10.4230/LIPIcs.SoCG.2026.63},
  annote =	{Keywords: graph drawing, topological graph, bipartite geometric graph, forbidden subgraph, extremal graph, thrackle}
}

Document

DOI: 10.4230/LIPIcs.SoCG.2026.79

D-GRIL: End-To-End Topological Learning with 2-Parameter Persistence

Authors: Soham Mukherjee, Shreyas N. Samaga, Cheng Xin, Steve Oudot, and Tamal K. Dey

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

Abstract

End-to-end topological learning using 1-parameter persistence is well-known. We show that the framework can be enhanced using 2-parameter persistence by adopting a recently introduced 2-parameter persistence based vectorization technique called Gril. We establish a theory for gradient descent on Gril producing D-Gril. We show that D-Gril can be used to learn a bifiltration function on benchmark graph datasets. Further, we exhibit that this framework can be applied in the context of bio-activity prediction in drug discovery.

Cite as

Soham Mukherjee, Shreyas N. Samaga, Cheng Xin, Steve Oudot, and Tamal K. Dey. D-GRIL: End-To-End Topological Learning with 2-Parameter Persistence. In 42nd International Symposium on Computational Geometry (SoCG 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 367, pp. 79:1-79:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{mukherjee_et_al:LIPIcs.SoCG.2026.79,
  author =	{Mukherjee, Soham and Samaga, Shreyas N. and Xin, Cheng and Oudot, Steve and Dey, Tamal K.},
  title =	{{D-GRIL: End-To-End Topological Learning with 2-Parameter Persistence}},
  booktitle =	{42nd International Symposium on Computational Geometry (SoCG 2026)},
  pages =	{79:1--79:17},
  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.79},
  URN =		{urn:nbn:de:0030-drops-258865},
  doi =		{10.4230/LIPIcs.SoCG.2026.79},
  annote =	{Keywords: Topological Data Analysis, Persistent Homology, Multiparameter Persistence, Graph Learning, Graph Neural Networks}
}

Document

DOI: 10.4230/LIPIcs.SoCG.2026.82

A Persistent Version of Latschev’s Theorem

Authors: Steve Oudot and Lukas Waas

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

Abstract

Latschev’s theorem provides sufficient conditions on a metric space M and δ > 0 for the homotopy type of M to agree with that of the Vietoris-Rips complex ℛ^δ(𝕄) of any nearby space 𝕄 in the Gromov-Hausdorff distance. We prove a persistent version of this theorem, providing sufficient conditions on a pair (M, f:M → ℝ^N) and δ > 0 for the persistent homotopy type of the sublevel set filtration of (M, f) to be interleaved with that of the function-Rips complex ℛ^δ(𝕄^•) of any nearby pair (𝕄, 𝕗). In particular, our result answers a longstanding question on the related topic of estimating sublevel set persistent homology from finite point samples.

Cite as

Steve Oudot and Lukas Waas. A Persistent Version of Latschev’s Theorem. In 42nd International Symposium on Computational Geometry (SoCG 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 367, pp. 82:1-82:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{oudot_et_al:LIPIcs.SoCG.2026.82,
  author =	{Oudot, Steve and Waas, Lukas},
  title =	{{A Persistent Version of Latschev’s Theorem}},
  booktitle =	{42nd International Symposium on Computational Geometry (SoCG 2026)},
  pages =	{82:1--82:17},
  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.82},
  URN =		{urn:nbn:de:0030-drops-258891},
  doi =		{10.4230/LIPIcs.SoCG.2026.82},
  annote =	{Keywords: Topological data analysis (TDA), metric geometry, Vietoris-Rips complex, homotopy theory, multi-parameter persistent homology}
}

Document

DOI: 10.4230/LIPIcs.SoCG.2026.93

Simplicial Approximation to CW Complexes with Spherical Delaunay Triangulations

Authors: Raphaël Tinarrage

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

Abstract

Simplicial approximation provides a framework for constructing simplicial complexes that are homotopy equivalent to a given manifold, provided a CW structure is explicitly known. However, its conventional implementation quickly becomes intractable on a computer: barycentric subdivision produces poorly shaped simplices, and the star condition introduces many vertices. To address these limitations, this article develops a subdivision scheme based on spherical Delaunay triangulations, which attains better refinement properties than barycentric subdivisions. Moreover, the star condition is reframed as two independent problems, one geometric and the other combinatorial, respectively tackled in the language of locally equiconnected spaces and the list homomorphism problem, allowing an exponential reduction in the number of vertices. Via a prototype implementation, we obtain simplicial complexes homotopy equivalent to Grassmannians and Stiefel manifolds up to dimension 5.

Cite as

Raphaël Tinarrage. Simplicial Approximation to CW Complexes with Spherical Delaunay Triangulations. In 42nd International Symposium on Computational Geometry (SoCG 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 367, pp. 93:1-93:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{tinarrage:LIPIcs.SoCG.2026.93,
  author =	{Tinarrage, Rapha\"{e}l},
  title =	{{Simplicial Approximation to CW Complexes with Spherical Delaunay Triangulations}},
  booktitle =	{42nd International Symposium on Computational Geometry (SoCG 2026)},
  pages =	{93:1--93:22},
  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.93},
  URN =		{urn:nbn:de:0030-drops-258991},
  doi =		{10.4230/LIPIcs.SoCG.2026.93},
  annote =	{Keywords: Triangulation of manifolds, Simplicial approximation, CW complexes, Delaunay complexes, List homomorphism problem, Topological Data Analysis}
}

Document

DOI: 10.4230/LIPIcs.FUN.2026.5

Token Positional Games

Authors: Guillaume Bagan, Quentin Deschamps, Florian Galliot, Mirjana Mikalački, and Nacim Oijid

Published in: LIPIcs, Volume 366, 13th International Conference on Fun with Algorithms (FUN 2026)

Abstract

The classical Maker-Breaker positional game is played on a board which is a hypergraph ℋ, with two players, Maker and Breaker, alternately claiming vertices of ℋ until all the vertices are claimed. When the game ends, Maker wins if she has claimed all the vertices of some edge of ℋ; otherwise, Breaker wins. Playing this game in real life can be done by placing tokens on the vertices of the board. In this paper, we study the unfortunate case in which one or both players do not have enough tokens to cover all the vertices and, as such, will have to move their tokens around at some point instead of placing new ones. There may be a bias, in that Maker and Breaker do not necessarily have the same amount of tokens. The present paper initiates the study of this generalization of positional games, called token positional games. A particularly interesting case is when Maker has a winning strategy in the classical game: what is the lowest number of tokens with which she still wins against Breaker’s unlimited stock? We notably show that, for k-uniform hypergraphs on an arbitrarily large number n of vertices, this number equals k if k ∈ {2,3} but can vary from k to Ω(n) if k ≥ 4. From an algorithmic point of view, PSPACE-hardness in general is inherited from classical positional games, but we get a polynomial-time algorithm to solve the case where Breaker only has one token. We also establish EXPTIME-completeness for a "token sliding" variation of the game.

Cite as

Guillaume Bagan, Quentin Deschamps, Florian Galliot, Mirjana Mikalački, and Nacim Oijid. Token Positional Games. In 13th International Conference on Fun with Algorithms (FUN 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 366, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bagan_et_al:LIPIcs.FUN.2026.5,
  author =	{Bagan, Guillaume and Deschamps, Quentin and Galliot, Florian and Mikala\v{c}ki, Mirjana and Oijid, Nacim},
  title =	{{Token Positional Games}},
  booktitle =	{13th International Conference on Fun with Algorithms (FUN 2026)},
  pages =	{5:1--5:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-417-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{366},
  editor =	{Iacono, John},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2026.5},
  URN =		{urn:nbn:de:0030-drops-257240},
  doi =		{10.4230/LIPIcs.FUN.2026.5},
  annote =	{Keywords: positional games, token games, hypergraphs, algorithmic complexity}
}

Document

DOI: 10.4230/OASIcs.NINeS.2026.17

Don’t Get Caught, Keep Your Onions in a Vault

Authors: Humza Ikram, Rumaisa Habib, Muaz Ali, and Zartash Afzal Uzmi

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

Abstract

When web applications wish to operate anonymously, they routinely host themselves as "Hidden Services" in the Tor network. However, these services are frequently threatened by deanonymization attacks, whereby their IP address and location may be inferred by the authorities. We present VaulTor, a novel architecture for the Tor network that ensures an extra layer of security for the Hidden Services against deanonymization attacks. In this new architecture, a volunteer (vault) is incentivized to host the web application content on behalf of the Hidden Service. The vault runs the hosted application in a Trusted Execution Environment (TEE) and becomes the point of contact for interested clients. This setup can substantially reduce the uptime requirement of the original Hidden Service provider, thereby significantly decreasing the chance of deanonymization attacks against them. Using a vault node in place of the hidden service node does not cause any noticeable performance degradation when accessing the hosted content.

Cite as

Humza Ikram, Rumaisa Habib, Muaz Ali, and Zartash Afzal Uzmi. Don’t Get Caught, Keep Your Onions in a Vault. In 1st New Ideas in Networked Systems (NINeS 2026). Open Access Series in Informatics (OASIcs), Volume 139, pp. 17:1-17:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ikram_et_al:OASIcs.NINeS.2026.17,
  author =	{Ikram, Humza and Habib, Rumaisa and Ali, Muaz and Uzmi, Zartash Afzal},
  title =	{{Don’t Get Caught, Keep Your Onions in a Vault}},
  booktitle =	{1st New Ideas in Networked Systems (NINeS 2026)},
  pages =	{17:1--17:24},
  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.17},
  URN =		{urn:nbn:de:0030-drops-256027},
  doi =		{10.4230/OASIcs.NINeS.2026.17},
  annote =	{Keywords: Tor, anonymity, Hidden Services, Trusted Execution Environments}
}

Document

DOI: 10.4230/OASIcs.NINeS.2026.19

Simulate Before Sending: Rethinking Transport in Datacenter Networks

Authors: Dan Straussman, Isaac Keslassy, Alexander Shpiner, and Liran Liss

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

Abstract

Existing transport protocols in commodity datacenter networks struggle to provide low collective completion times (CCTs) to AI training collectives, as packet losses and retransmissions significantly degrade performance. We propose dcSim, an efficient transport that achieves low CCTs and practically lossless performance with commodity switches. In dcSim, each packet first employs a small simulation probe to traverse the network and explore congestion along a candidate path. Only packets whose simulation probes succeed are then transmitted, expecting to succeed as well. Evaluations confirm that dcSim achieves faster CCTs than existing schemes, with small queues and virtually zero packet loss. Finally, dcSim also excels in adverse conditions, including oversubscribed topologies.

Cite as

Dan Straussman, Isaac Keslassy, Alexander Shpiner, and Liran Liss. Simulate Before Sending: Rethinking Transport in Datacenter Networks. In 1st New Ideas in Networked Systems (NINeS 2026). Open Access Series in Informatics (OASIcs), Volume 139, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{straussman_et_al:OASIcs.NINeS.2026.19,
  author =	{Straussman, Dan and Keslassy, Isaac and Shpiner, Alexander and Liss, Liran},
  title =	{{Simulate Before Sending: Rethinking Transport in Datacenter Networks}},
  booktitle =	{1st New Ideas in Networked Systems (NINeS 2026)},
  pages =	{19:1--19:22},
  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.19},
  URN =		{urn:nbn:de:0030-drops-256044},
  doi =		{10.4230/OASIcs.NINeS.2026.19},
  annote =	{Keywords: Datacenter networks, transport protocols, AI training, lossless networks}
}

Document

DOI: 10.4230/LIPIcs.STACS.2026.36

Time-Optimal Construction of String Synchronizing Sets

Authors: Jonas Ellert and Tomasz Kociumaka

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

Abstract

A powerful design principle behind many modern string algorithms is local consistency: breaking the symmetry between string positions based on their small contexts so that matching fragments are handled consistently. Among the most influential instantiations of this principle are string synchronizing sets [Kempa & Kociumaka; STOC 2019]. A τ-synchronizing set of a string of length n is a set of O(n/τ) string positions, chosen using their length-2τ contexts, such that (outside of highly periodic regions) every block of τ consecutive positions contains at least one element of the set. Synchronizing sets have found dozens of applications in diverse settings, from quantum and dynamic algorithms to fully compressed computation. In the classic word RAM model, particularly for strings over small alphabets, they enabled faster solutions to core problems in data compression, text indexing, and string similarity. In this work, we show that any string T ∈ [0 .. σ)ⁿ can be preprocessed in O(n log σ / log n) time so that, for any given integer τ ∈ [1 .. n], a τ-synchronizing set of T can be constructed in O((n log τ)/(τ log n)) time. Both bounds are optimal in the word RAM model with machine word size w = Θ(log n), matching the information-theoretic minimum for the input and output sizes, respectively. Previously, constructing a τ-synchronizing set required O(n/τ) time after an O(n)-time preprocessing [Kociumaka, Radoszewski, Rytter, and Waleń; SICOMP 2024], or, in the restricted regime of τ < 0.2 log_σ n, without any preprocessing needed [Kempa & Kociumaka; STOC 2019]. A simple instantiation of our method outputs the synchronizing set as a sorted list in O(n/τ) time, or as a bitmask in O(n/log n) time. Our optimal construction produces a compact fully indexable dictionary, supporting select queries in O(1) time and rank queries in O(log ((log τ)/(log log n))) time. The latter complexity matches known unconditional cell-probe lower bounds for τ ≤ n^{1-Ω(1)}. To achieve this, we introduce a general framework for efficiently processing sparse integer sequences via a custom variable-length encoding. We also augment the optimal variant of van Emde Boas trees [Pătraşcu & Thorup; STOC 2006] with a deterministic linear-time construction. When the set is represented as a bitmask under our sparse encoding, the same guarantees for select and rank queries hold after preprocessing in time proportional to the size of our encoding (in words).

Cite as

Jonas Ellert and Tomasz Kociumaka. Time-Optimal Construction of String Synchronizing Sets. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 36:1-36:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ellert_et_al:LIPIcs.STACS.2026.36,
  author =	{Ellert, Jonas and Kociumaka, Tomasz},
  title =	{{Time-Optimal Construction of String Synchronizing Sets}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{36:1--36:22},
  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.36},
  URN =		{urn:nbn:de:0030-drops-255258},
  doi =		{10.4230/LIPIcs.STACS.2026.36},
  annote =	{Keywords: synchronizing sets, local consistency, packed strings}
}

Document

DOI: 10.4230/LIPIcs.STACS.2026.53

Maximum Reachability Orientation of Mixed Graphs

Authors: Florian Hörsch

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

Abstract

We aim to find orientations of mixed graphs optimizing the total reachability, a problem that has applications in causality and biology. For given a digraph D, we use P(D) for the set of ordered pairs of distinct vertices in V(D) and we define κ_D:P(D) → {0,1} by κ_D(u,v) = 1 if v is reachable from u in D, and κ_D(u,v) = 0, otherwise. We use R(D) = ∑_{(u,v) ∈ P(D)}κ_D(u,v). Now, given a mixed graph G, we aim to find an orientation x⃑{G} of G that maximizes R(x⃑{G}). Hakimi, Schmeichel, and Young proved that the problem can be solved in polynomial time when restricted to undirected inputs. They inquired about the complexity in mixed graphs. We answer this question by showing that this problem is NP-hard, and, moreover, APX-hard. We then develop a finer understanding of how quickly the problem becomes difficult when going from undirected to mixed graphs. To this end, we consider the parameterized complexity of the problem with respect to the number k of preoriented arcs of G, a poorly studied form of parameterization. We show that the problem can be solved in time n^{O(k)} and that a (1-ε)-approximation can be computed in time f(k,ε)n^{O(1)} for any ε > 0.

Cite as

Florian Hörsch. Maximum Reachability Orientation of Mixed Graphs. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 53:1-53:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{horsch:LIPIcs.STACS.2026.53,
  author =	{H\"{o}rsch, Florian},
  title =	{{Maximum Reachability Orientation of Mixed Graphs}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{53:1--53: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.53},
  URN =		{urn:nbn:de:0030-drops-255421},
  doi =		{10.4230/LIPIcs.STACS.2026.53},
  annote =	{Keywords: orientations, mixed graphs, reachability, parameterized complexity, approximation}
}

Document

DOI: 10.4230/LIPIcs.STACS.2026.8

On the p-adic Skolem Problem

Authors: Piotr Bacik, Joël Ouaknine, David Purser, and James Worrell

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

Abstract

The Skolem Problem asks to determine whether a given linear recurrence sequence (LRS) has a zero term. Showing decidability of this problem is equivalent to giving an effective proof of the Skolem-Mahler-Lech Theorem, which asserts that a non-degenerate LRS has finitely many zeros. The latter result was proven over 90 years ago via an ineffective method showing that such an LRS has only finitely many p-adic zeros. In this paper we consider the problem of determining whether a given LRS has a p-adic zero, as well as the corresponding function problem of computing exact representations of all p-adic zeros. We present algorithms for both problems and report on their implementation. The output of the algorithms is unconditionally correct, and termination is guaranteed subject to the p-adic Schanuel Conjecture (a standard number-theoretic hypothesis concerning the p-adic exponential function). While these algorithms do not solve the Skolem Problem, they can be exploited to find natural-number and rational zeros under additional hypotheses. To illustrate this, we apply our results to show decidability of the Simultaneous Skolem Problem (determine whether two coprime linear recurrences have a common natural-number zero), again subject to the p-adic Schanuel Conjecture.

Cite as

Piotr Bacik, Joël Ouaknine, David Purser, and James Worrell. On the p-adic Skolem Problem. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bacik_et_al:LIPIcs.STACS.2026.8,
  author =	{Bacik, Piotr and Ouaknine, Jo\"{e}l and Purser, David and Worrell, James},
  title =	{{On the p-adic Skolem Problem}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{8:1--8:20},
  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.8},
  URN =		{urn:nbn:de:0030-drops-254979},
  doi =		{10.4230/LIPIcs.STACS.2026.8},
  annote =	{Keywords: Skolem Problem, p-adic Schanuel Conjecture, Skolem Conjecture, Exponential Local-Global Principle, exponential polynomial}
}

Document

DOI: 10.4230/LIPIcs.CSL.2026.16

On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions

Authors: Nicolas Peltier

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

Abstract

Separation Logic (SL) is a well-established framework for reasoning about programs that manipulate dynamic memory. To express and verify properties of custom recursive data structures, SL is extended with spatial predicates defined by user-specified inductive rules. Many verification problems reduce to deciding entailments between formulas involving these predicates. While the general entailment problem is undecidable, a broad class of inductive rules - known as PCE (Progressing, Connected, and Established) - has been identified for which entailment is decidable. In this work, we extend the study of the entailment problem to Dynamic Separation Logic (DSL), an extension of SL that includes dynamic modalities for reasoning about actions on the heap and store. We show that entailment in DSL remains decidable for PCE rules by proving that dynamic modalities can be automatically eliminated.

Cite as

Nicolas Peltier. On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{peltier:LIPIcs.CSL.2026.16,
  author =	{Peltier, Nicolas},
  title =	{{On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{16:1--16:20},
  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.16},
  URN =		{urn:nbn:de:0030-drops-254402},
  doi =		{10.4230/LIPIcs.CSL.2026.16},
  annote =	{Keywords: Separation logic, Dynamic logic, Entailment problem}
}

74 Search Results for "Frank, Florian"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message