7 Search Results for "Hansen, Nils"

Document
DOI: 10.4230/LIPIcs.CPM.2026.20
Longest Common Extension of a Dynamic String in Parallel Constant Time

Authors: Daniel Alexander Albert

Published in: LIPIcs, Volume 369, 37th Annual Symposium on Combinatorial Pattern Matching (CPM 2026)

Abstract
A longest common extension (LCE) query on a string computes the length of the longest common suffix or prefix at two given positions. A dynamic LCE algorithm maintains a data structure that allows efficient LCE queries on a string that can change via character insertions and deletions. A dynamic parallel constant-time algorithm is presented that can maintain LCE queries on a common CRCW PRAM with 𝒪(n^ε) work, for any ε > 0. The algorithm maintains a string synchronizing sets hierarchy, which it uses to answer substring equality queries, which it in turn uses to answer LCE queries. To achieve constant runtime, the algorithm allows parts of its information to become outdated by up to log n log^* n updates. It answers queries by combining this slightly outdated information with a list of the recent changes. Two applications of this dynamic LCE algorithm are shown. Firstly, a dynamic parallel constant-time algorithm can maintain membership in a Dyck language D_k, k > 0 with 𝒪(n^ε) work for any ε > 0. Secondly, a dynamic parallel constant-time algorithm can maintain squares with 𝒪(n^ε) work for any ε > 0.
Cite as

Daniel Alexander Albert. Longest Common Extension of a Dynamic String in Parallel Constant Time. In 37th Annual Symposium on Combinatorial Pattern Matching (CPM 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 369, pp. 20:1-20:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{albert:LIPIcs.CPM.2026.20,
  author =	{Albert, Daniel Alexander},
  title =	{{Longest Common Extension of a Dynamic String in Parallel Constant Time}},
  booktitle =	{37th Annual Symposium on Combinatorial Pattern Matching (CPM 2026)},
  pages =	{20:1--20:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-420-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{369},
  editor =	{Bille, Philip and Prezza, Nicola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CPM.2026.20},
  URN =		{urn:nbn:de:0030-drops-259467},
  doi =		{10.4230/LIPIcs.CPM.2026.20},
  annote =	{Keywords: Dynamic Strings, Work, Parallel Constant Time, Longest Common Extension, Longest Common Prefix}
}
Document
DOI: 10.4230/LIPIcs.STACS.2026.14
Computing Tarski Fixed Points in Financial Networks

Authors: Leander Besting, Martin Hoefer, and Lars Huth

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

Abstract
Modern financial networks are highly connected and result in complex interdependencies of the involved institutions. In the prominent Eisenberg-Noe model [Eisenberg and Noe, 2001], a fundamental aspect is clearing - to determine the amount of assets available to each financial institution in the presence of potential defaults and bankruptcy. A clearing state represents a fixed point that satisfies a set of natural axioms. Existence can be established (even in broad generalizations of the model) using Tarski’s theorem. While a maximal fixed point can be computed in polynomial time, the complexity of computing other fixed points is open. In this paper, we provide an efficient algorithm to compute a minimal fixed point. Our algorithm applies in a broad generalization of the Eisenberg-Noe model with any monotone, piecewise-linear payment functions and default costs. We also study claims trading, a local network adjustment to improve clearing, when networks are evaluated with minimal clearing. We provide an efficient algorithm to decide existence of Pareto-improving trades and compute optimal ones if they exist.
Cite as

Leander Besting, Martin Hoefer, and Lars Huth. Computing Tarski Fixed Points in Financial Networks. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{besting_et_al:LIPIcs.STACS.2026.14,
  author =	{Besting, Leander and Hoefer, Martin and Huth, Lars},
  title =	{{Computing Tarski Fixed Points in Financial Networks}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{14:1--14:18},
  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.14},
  URN =		{urn:nbn:de:0030-drops-255038},
  doi =		{10.4230/LIPIcs.STACS.2026.14},
  annote =	{Keywords: Tarski Fixed Points, Financial Networks, Minimal Clearing, Claims Trade}
}
Document
DOI: 10.4230/LIPIcs.STACS.2026.31
Lower Bounds for Ranking-Based Pivot Rules

Authors: Yann Disser, Georg Loho, Matthew Maat, and Nils Mosis

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

Abstract
The existence of a polynomial pivot rule for the simplex method for linear programming, policy iteration for Markov decision processes, and strategy improvement for parity games each are prominent open problems in their respective fields. While numerous natural candidates for efficient rules have been eliminated, all existing lower bound constructions are tailored to individual or small sets of pivot rules. We introduce a unified framework for formalizing classes of rules according to the information about the input that they rely on. Within this framework, we show lower bounds for ranking-based classes of rules that base their decisions on orderings of the improving pivot steps induced by the underlying data. Our first result is a superpolynomial lower bound for strategy improvement, obtained via a family of sink parity games, which applies to memory-based generalizations of Bland’s rule that only access the input by comparing the ranks of improving edges in some global order. Our second result is a subexponential lower bound for policy iteration, obtained via a family of Markov decision processes, which applies to memoryless rules that only access the input by comparing improving actions according to their ranks in a global order, their reduced costs, and the associated improvements in objective value. Both results carry over to the simplex method for linear programming.
Cite as

Yann Disser, Georg Loho, Matthew Maat, and Nils Mosis. Lower Bounds for Ranking-Based Pivot Rules. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{disser_et_al:LIPIcs.STACS.2026.31,
  author =	{Disser, Yann and Loho, Georg and Maat, Matthew and Mosis, Nils},
  title =	{{Lower Bounds for Ranking-Based Pivot Rules}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{31:1--31:19},
  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.31},
  URN =		{urn:nbn:de:0030-drops-255207},
  doi =		{10.4230/LIPIcs.STACS.2026.31},
  annote =	{Keywords: lower bounds, Markov decision processes, parity games, pivot rules, policy iteration, simplex method}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.36
Verifying Datalog Reasoning with Lean

Authors: Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch

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

Abstract
Datalog is an essential logical rule language with many applications, and modern rule engines compute logical consequences for Datalog with high performance and scalability. While Datalog is rather simple and, in principle, explainable by design, such sophisticated implementations and optimizations are hard to verify. We therefore propose a certificate-based approach to validate results of Datalog reasoners in a formally verified checker for Datalog proofs. Using the proof assistant Lean, we implement such a checker and verify its correctness against direct formalizations of the Datalog semantics. We propose two JSON encodings for Datalog proofs: one using the widely supported Datalog proof trees, and one using directed acyclic graphs for succinctness. To evaluate the practical feasibility and performance of our approach, we validate proofs that we obtain by converting derivation traces of an existing Datalog reasoner into our tool-independent format.
Cite as

Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch. Verifying Datalog Reasoning with Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{tantow_et_al:LIPIcs.ITP.2025.36,
  author =	{Tantow, Johannes and Gerlach, Lukas and Mennicke, Stephan and Kr\"{o}tzsch, Markus},
  title =	{{Verifying Datalog Reasoning with Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{36:1--36:19},
  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.36},
  URN =		{urn:nbn:de:0030-drops-246342},
  doi =		{10.4230/LIPIcs.ITP.2025.36},
  annote =	{Keywords: Certifying Algorithms, Datalog, Formal Verification}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.146
Saturation Problems for Families of Automata

Authors: León Bohn, Yong Li, Christof Löding, and Sven Schewe

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Families of deterministic finite automata (FDFA) represent regular ω-languages through their ultimately periodic words (UP-words). An FDFA accepts pairs of words, where the first component corresponds to a prefix of the UP-word, and the second component represents a period of that UP-word. An FDFA is termed saturated if, for each UP-word, either all or none of the pairs representing that UP-word are accepted. We demonstrate that determining whether a given FDFA is saturated can be accomplished in polynomial time, thus improving the known PSPACE upper bound by an exponential. We illustrate the application of this result by presenting the first polynomial learning algorithms for representations of the class of all regular ω-languages. Furthermore, we establish that deciding a weaker property, referred to as almost saturation, is PSPACE-complete. Since FDFAs do not necessarily define regular ω-languages when they are not saturated, we also address the regularity problem and show that it is PSPACE-complete. Finally, we explore a variant of FDFAs called families of deterministic weak automata (FDWA), where the semantics for the periodic part of the UP-word considers ω-words instead of finite words. We demonstrate that saturation for FDWAs is also decidable in polynomial time, that FDWAs always define regular ω-languages, and we compare the succinctness of these different models.
Cite as

León Bohn, Yong Li, Christof Löding, and Sven Schewe. Saturation Problems for Families of Automata. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 146:1-146:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bohn_et_al:LIPIcs.ICALP.2025.146,
  author =	{Bohn, Le\'{o}n and Li, Yong and L\"{o}ding, Christof and Schewe, Sven},
  title =	{{Saturation Problems for Families of Automata}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{146:1--146:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.146},
  URN =		{urn:nbn:de:0030-drops-235239},
  doi =		{10.4230/LIPIcs.ICALP.2025.146},
  annote =	{Keywords: Families of Automata, automata learning, FDFAs}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.34
Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering

Authors: Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, and Yulei Sui

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

Abstract
Abstract interpretation provides a foundational framework for approximating program semantics by interpreting code through abstract domains using semantic functions over ordered sets along a program’s control flow graph (CFG). To facilitate fixpoint computation in abstract interpretation, weak topological ordering (WTO) is an effective strategy for handling loops, as it identifies strategic control points in the CFG where widening and narrowing operations should be applied. However, existing abstract interpreters still face challenges when extending WTO computation in the presence of recursive programs. Computing a precise whole-program WTO requires full context-sensitive analysis which is not scalable for large programs, while context-insensitive analysis introduces spurious cycles that compromise precision. Current approaches either ignore recursion (resulting in unsoundness) or rely on conservative approximations, sacrificing precision by adopting the greatest elements of abstract domains and applying widening at function boundaries without subsequent narrowing refinements. These can lead to undesired results for downstream tasks, such as bug detection. To address the above limitations, we present RecTopo, a new technique to boost the efficiency of precise abstract interpretation in the presence of recursive programs through interprocedural weak topological ordering (IWTO). Rather than pursuing an expensive whole-program WTO analysis, RecTopo employs an on-demand approach that strategically decomposes programs at recursion boundaries and constructs targeted IWTOs for each recursive component. RecTopo dissects and analyzes (nested) recursions through interleaved widening and narrowing operations. This approach enables precise control over interpretation ordering within recursive structures while eliminating spurious recursions through systematic correlation of control flow and call graphs. We implemented RecTopo and evaluated its effectiveness using an assertion-based checking client focused on buffer overflow detection, comparing it against three popular open-source abstract interpreters (IKOS, Clam, CSA). The experiments on 8312 programs from the NIST dataset demonstrate that, on average, RecTopo is 31.99% more precise and achieves a 17.49% higher recall rate compared to three other tools. Moreover, RecTopo exhibits an average precision improvement of 46.51% and a higher recall rate of 32.98% compared to our baselines across ten large open-source projects. Further ablation studies reveal that IWTO reduces spurious widening operations compared to whole-program WTO, resulting in a 12.83% reduction in analysis time.
Cite as

Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, and Yulei Sui. Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 34:1-34:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.ECOOP.2025.34,
  author =	{Yang, Jiawei and Cheng, Xiao and Chang, Bor-Yuh Evan and Luo, Xiapu and Sui, Yulei},
  title =	{{Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{34:1--34:31},
  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.34},
  URN =		{urn:nbn:de:0030-drops-233265},
  doi =		{10.4230/LIPIcs.ECOOP.2025.34},
  annote =	{Keywords: Abstract interpretation, recursion, weak topological ordering}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2023.5
Modular Abstract Definitional Interpreters for WebAssembly

Authors: Katharina Brandl, Sebastian Erdweg, Sven Keidel, and Nils Hansen

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Even though static analyses can improve performance and secure programs against vulnerabilities, no static whole-program analyses exist for WebAssembly (Wasm) to date. Part of the reason is that Wasm has many complex language concerns, and it is not obvious how to adopt existing analysis frameworks for these features. This paper explores how abstract definitional interpretation can be used to develop sophisticated analyses for Wasm and other complex languages efficiently. In particular, we show that the semantics of Wasm can be decomposed into 19 language-independent components that abstract different aspects of Wasm. We have written a highly configurable definitional interpreter for full Wasm 1.0 in 1628 LOC against these components. Analysis developers can instantiate this interpreter with different value and effect abstractions to obtain abstract definitional interpreters that compute inter-procedural control and data-flow information. This way, we develop the first whole-program dead code, constant propagation, and taint analyses for Wasm, each in less than 210 LOC. We evaluate our analyses on 1458 Wasm binaries collected by others in the wild. Our implementation is based on a novel framework for definitional abstract interpretation in Scala that eliminates scalability issues of prior work.
Cite as

Katharina Brandl, Sebastian Erdweg, Sven Keidel, and Nils Hansen. Modular Abstract Definitional Interpreters for WebAssembly. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 5:1-5:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{brandl_et_al:LIPIcs.ECOOP.2023.5,
  author =	{Brandl, Katharina and Erdweg, Sebastian and Keidel, Sven and Hansen, Nils},
  title =	{{Modular Abstract Definitional Interpreters for WebAssembly}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{5:1--5:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.5},
  URN =		{urn:nbn:de:0030-drops-181982},
  doi =		{10.4230/LIPIcs.ECOOP.2023.5},
  annote =	{Keywords: Static Analysis, WebAssembly}
}
  • Refine by Type
  • 7 Document/PDF
  • 6 Document/HTML

  • Refine by Publication Year
  • 3 2026
  • 3 2025
  • 1 2023

  • Refine by Author
  • 1 Albert, Daniel Alexander
  • 1 Besting, Leander
  • 1 Bohn, León
  • 1 Brandl, Katharina
  • 1 Chang, Bor-Yuh Evan
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs

  • Refine by Classification
  • 1 Computing methodologies → Theorem proving algorithms
  • 1 Mathematics of computing → Combinatorial algorithms
  • 1 Networks → Network algorithms
  • 1 Software and its engineering → Automated static analysis
  • 1 Software and its engineering → Formal software verification
  • Show More...

  • Refine by Keyword
  • 1 Abstract interpretation
  • 1 Certifying Algorithms
  • 1 Claims Trade
  • 1 Datalog
  • 1 Dynamic Strings
  • 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