11 Search Results for "Bernard, Sophie"

Document
DOI: 10.4230/LIPIcs.STACS.2026.73
Colouring Probe H-Free Graphs

Authors: Daniël Paulusma, Johannes Rauch, and Erik Jan van Leeuwen

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

Abstract
The NP-complete problems Colouring and k-Colouring (k ≥ 3) are well studied on H-free graphs, i.e., graphs that do not contain some fixed graph H as an induced subgraph. We research to what extent the known polynomial-time algorithms for H-free graphs can be generalized if we only know some of the edges of the input graph. We do this by considering the classical probe graph model introduced in the early nineties. For a graph H, a partitioned probe H-free graph (G,P,N) consists of a graph G = (V,E), together with a set P ⊆ V of probes and an independent set N = V ⧵ P of non-probes, such that G+F is H-free for some edge set F ⊆ binom(N,2). We show the following: - We fully classify Colouring on partitioned probe H-free graphs and show that the obtained complexity dichotomy differs from the known dichotomy of Colouring for H-free graphs. - We fully classify 3-Colouring on partitioned probe P_t-free graphs: we prove polynomial-time solvability for t ≤ 5 and NP-completeness for t ≥ 6. In contrast, 3-Colouring on P_t-free graphs is known to be polynomial-time solvable for t ≤ 7 and quasi-polynomial-time solvable for t ≥ 8. Our main result is our polynomial-time algorithm for 3-Colouring on partitioned P₅-free graphs. For this result, and also for all our other polynomial-time results, we do not need to know the edge set F; we only need to know its existence. Moreover, the class of probe P₅-free graphs includes not only paths of arbitrary length but even all bipartite graphs and is much richer than the class of P₅-free graphs. The latter is also evidenced by the fact that there exist graph problems, such as Matching Cut, that are known to be polynomial-time solvable for P₅-free graphs but NP-complete for partitioned probe P₅-free graphs. In particular, unlike the class of 3-colourable P₅-free graphs, the class of 3-colourable probe P₅-free graphs has unbounded mim-width. Hence, our polynomial-time result for 3-Colouring for probe P₅-free graphs suggests that there may be another, deeper overarching reason why 3-Colouring is polynomial-time solvable for P₅-free graphs.
Cite as

Daniël Paulusma, Johannes Rauch, and Erik Jan van Leeuwen. Colouring Probe H-Free Graphs. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 73:1-73:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{paulusma_et_al:LIPIcs.STACS.2026.73,
  author =	{Paulusma, Dani\"{e}l and Rauch, Johannes and van Leeuwen, Erik Jan},
  title =	{{Colouring Probe H-Free Graphs}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{73:1--73: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.73},
  URN =		{urn:nbn:de:0030-drops-255621},
  doi =		{10.4230/LIPIcs.STACS.2026.73},
  annote =	{Keywords: colouring, probe graph, forbidden induced subgraph, complexity dichotomy}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.14
Canonical for Automated Theorem Proving in Lean

Authors: Chase Norman and Jeremy Avigad

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

Abstract
Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to generate proof terms and synthesize programs. The tactic supports higher-order and dependently-typed goals, structural recursion over indexed inductive types, and definitional equality. Canonical finds proofs for 84% of Natural Number Game problems in 51 seconds total.
Cite as

Chase Norman and Jeremy Avigad. Canonical for Automated Theorem Proving in Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{norman_et_al:LIPIcs.ITP.2025.14,
  author =	{Norman, Chase and Avigad, Jeremy},
  title =	{{Canonical for Automated Theorem Proving in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{14:1--14:20},
  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.14},
  URN =		{urn:nbn:de:0030-drops-246128},
  doi =		{10.4230/LIPIcs.ITP.2025.14},
  annote =	{Keywords: Automated Reasoning, Interactive Theorem Proving, Dependent Type Theory, Inhabitation, Unification, Program Synthesis, Formal Methods}
}
Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.1
Human-AI Interaction in Space: Insights from a Mars Analog Mission with the Harmony Large Language Model

Authors: Hippolyte Hilgers, Jean Vanderdonckt, and Radu-Daniel Vatavu

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)

Abstract
The operational complexities of space missions require reliable, context-aware technical assistance for astronauts, especially when technical expertise is not available onboard and communication with Earth is delayed or limited. In this context, Large Language Models present a promising opportunity to augment human capabilities. To this end, we present Harmony, a model designed to provide astronauts with real-time technical assistance, fostering human-AI collaboration during analog missions. We report empirical results from an experiment involving seven analog astronauts that evaluated their user experience with Harmony in both a conventional environment and an isolated, confined, and extreme physical setting at the Mars Desert Research Station over four sessions, and discuss how the Mars analog environment impacted their experience. Our findings reveal the extent to which human-AI interactions evolve across various user experience dimensions and suggest how Harmony can be further adapted to suit extreme environments, with a focus on SpaceCHI.
Cite as

Hippolyte Hilgers, Jean Vanderdonckt, and Radu-Daniel Vatavu. Human-AI Interaction in Space: Insights from a Mars Analog Mission with the Harmony Large Language Model. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hilgers_et_al:OASIcs.SpaceCHI.2025.1,
  author =	{Hilgers, Hippolyte and Vanderdonckt, Jean and Vatavu, Radu-Daniel},
  title =	{{Human-AI Interaction in Space: Insights from a Mars Analog Mission with the Harmony Large Language Model}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{1:1--1:20},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.1},
  URN =		{urn:nbn:de:0030-drops-239912},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.1},
  annote =	{Keywords: Extreme user experience, Human-AI interaction, Isolated-confined-extreme environment, Interaction design, Large Language Models, Mars Desert Research Station, Space mission, Technical assistance, Technical documentation, User experience}
}
Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.18
Advancing Intelligent Personal Assistants for Human Spaceflight

Authors: Leonie Bensch, Oliver Bensch, and Tommy Nilsson

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)

Abstract
The Artemis program and upcoming missions to Mars mark a new era of human space exploration that will require new tools to support astronaut autonomy in the absence of real-time communication with Earth. This paper investigates the role of voice-based intelligent personal assistants (IPAs) in future crewed space missions. Through semi-structured interviews with astronauts (n=3) and spaceflight experts (n=12), we identify key user-centered design requirements for IPAs in this uniquely constrained and safety-critical environment. Our thematic analysis reveals core requirements for flexibility, reliability, offline capability, and multimodal interaction. Drawing on these findings, we outline design guidelines for next-generation IPAs and discuss how technologies such as retrieval-augmented generation (RAG), knowledge graphs, and augmented reality should be combined to support flexible, reliable, and multimodal IPAs for future human spaceflight missions.
Cite as

Leonie Bensch, Oliver Bensch, and Tommy Nilsson. Advancing Intelligent Personal Assistants for Human Spaceflight. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bensch_et_al:OASIcs.SpaceCHI.2025.18,
  author =	{Bensch, Leonie and Bensch, Oliver and Nilsson, Tommy},
  title =	{{Advancing Intelligent Personal Assistants for Human Spaceflight}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{18:1--18:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.18},
  URN =		{urn:nbn:de:0030-drops-240082},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.18},
  annote =	{Keywords: Conversational Assistant, Intelligent Personal Assistant, Artificial Intelligence, Astronaut, Human Spaceflight, Generative Pre-Trained Transformer (GPT), Retrieval Augmented Generation (RAG), Knowledge Graphs, Augmented Reality, Voice Assistant, Long Duration Spaceflight}
}
Document
APPROX
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2025.15
A Polynomial-Time Approximation Algorithm for Complete Interval Minors

Authors: Romain Bourneuf, Julien Cocquet, Chaoliang Tang, and Stéphan Thomassé

Published in: LIPIcs, Volume 353, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)

Abstract
As shown by Robertson and Seymour, deciding whether the complete graph K_t is a minor of an input graph G is a fixed parameter tractable problem when parameterized by t. From the approximation viewpoint, a substantial gap remains: there is no PTAS for finding the largest complete minor unless P = NP, whereas the best known result is a polytime O(√ n)-approximation algorithm by Alon, Lingas and Wahlén. We investigate the complexity of finding K_t as interval minor in ordered graphs (i.e. graphs with a linear order on the vertices, in which intervals are contracted to form minors). Our main result is a polytime f(t)-approximation algorithm, where f is triply exponential in t but independent of n. The algorithm is based on delayed decompositions and shows that ordered graphs without a K_t interval minor can be constructed via a bounded number of three operations: closure under substitutions, edge union, and concatenation of a stable set. As a byproduct, graphs avoiding K_t as an interval minor have bounded chromatic number.
Cite as

Romain Bourneuf, Julien Cocquet, Chaoliang Tang, and Stéphan Thomassé. A Polynomial-Time Approximation Algorithm for Complete Interval Minors. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 353, pp. 15:1-15:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bourneuf_et_al:LIPIcs.APPROX/RANDOM.2025.15,
  author =	{Bourneuf, Romain and Cocquet, Julien and Tang, Chaoliang and Thomass\'{e}, St\'{e}phan},
  title =	{{A Polynomial-Time Approximation Algorithm for Complete Interval Minors}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)},
  pages =	{15:1--15:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-397-3},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{353},
  editor =	{Ene, Alina and Chattopadhyay, Eshan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2025.15},
  URN =		{urn:nbn:de:0030-drops-243814},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2025.15},
  annote =	{Keywords: Approximation algorithm, Ordered graphs, Interval minors, Delayed decompositions}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.31
Games with ω-Automatic Preference Relations

Authors: Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin

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

Abstract
This paper investigates Nash equilibria (NEs) in multi-player turn-based games on graphs, where player preferences are modeled as ω-automatic relations via deterministic parity automata. Unlike much of the existing literature, which focuses on specific reward functions, our results apply to any preference relation definable by an ω-automatic relation. We analyze the computational complexity of determining the existence of an NE (possibly under some constraints), verifying whether a given strategy profile forms an NE, and checking whether a specific outcome can be realized by an NE. When a (constrained) NE exists, we show that there always exists one with finite-memory strategies. Finally, we explore fundamental properties of ω-automatic relations and their implications in the existence of equilibria.
Cite as

Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin. Games with ω-Automatic Preference Relations. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.MFCS.2025.31,
  author =	{Bruy\`{e}re, V\'{e}ronique and Grandmont, Christophe and Raskin, Jean-Fran\c{c}ois},
  title =	{{Games with \omega-Automatic Preference Relations}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{31:1--31:19},
  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.31},
  URN =		{urn:nbn:de:0030-drops-241381},
  doi =		{10.4230/LIPIcs.MFCS.2025.31},
  annote =	{Keywords: Games played on graphs, Nash equilibrium, \omega-automatic relations, \omega-recognizable relations, constrained Nash equilibria existence problem}
}
Document
DOI: 10.4230/LIPIcs.DNA.31.11
Leakless Polymerase-Dependent Strand Displacement Systems

Authors: Zoë Evelyn Mōhalakealoha Derauf and Chris Thachuk

Published in: LIPIcs, Volume 347, 31st International Conference on DNA Computing and Molecular Programming (DNA 31) (2025)

Abstract
A grand challenge facing molecular programmers is the rational development of fast, robust, and isothermal architectures akin to "chemical central processing units" that can sense (bio-)chemical signals from their environment, perform complex computation, and orchestrate a physical response in situ. DNA strand displacement systems (DSDs) remain a compelling candidate, but are hampered by spurious reaction pathways that lead to incorrect output. DSDs that utilize the systematic leakless motif can be made arbitrarily robust at the cost of increasing redundancy and network size (scaling), and thus a degradation of kinetic performance. Another class of architectures utilize DNA hybridization, extension, and signal production of entirely sequestered outputs via strand-displacing polymerases (SDPs) that have resulted in impressive demonstrations; however, they face similar challenges of aberrant behavior such as mis-priming by incorrect signals. Our work introduces a unified polymerase-dependent toehold-mediated strand displacement (PD-TMSD) architecture that integrates the programmed specificity of DSDs with the unique advantages of SDPs. This unification enables systems that can be made arbitrarily robust, at any concentration range, without increasing network size. We propose a number of gate designs and composition rules to compute arbitrary Boolean functions, emulate arbitrary chemical reaction networks, and explore time-bounded probabilistic computation made possible by certain classes of SDPs. Our theoretical exploration is backed by preliminary experimental demonstrations. This contribution was inspired by the belief that molecular programming can meet or exceed the complexity exhibited in biology if we embrace its best understood molecular machinery and couple it with systematic design principles built upon a strong theoretical foundation.
Cite as

Zoë Evelyn Mōhalakealoha Derauf and Chris Thachuk. Leakless Polymerase-Dependent Strand Displacement Systems. In 31st International Conference on DNA Computing and Molecular Programming (DNA 31). Leibniz International Proceedings in Informatics (LIPIcs), Volume 347, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{derauf_et_al:LIPIcs.DNA.31.11,
  author =	{Derauf, Zo\"{e} Evelyn M\={o}halakealoha and Thachuk, Chris},
  title =	{{Leakless Polymerase-Dependent Strand Displacement Systems}},
  booktitle =	{31st International Conference on DNA Computing and Molecular Programming (DNA 31)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-399-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{347},
  editor =	{Schaeffer, Josie and Zhang, Fei},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DNA.31.11},
  URN =		{urn:nbn:de:0030-drops-238608},
  doi =		{10.4230/LIPIcs.DNA.31.11},
  annote =	{Keywords: DNA strand displacement, strand-displacing polymerases, molecular computation, energy barriers, kinetics}
}
Document
DOI: 10.4230/LIPIcs.WABI.2025.7
Sequence Similarity Estimation by Random Subsequence Sketching

Authors: Ke Chen, Vinamratha Pattar, and Mingfu Shao

Published in: LIPIcs, Volume 344, 25th International Conference on Algorithms for Bioinformatics (WABI 2025)

Abstract
Sequence similarity estimation is essential for many bioinformatics tasks, including functional annotation, phylogenetic analysis, and overlap graph construction. Alignment-free methods aim to solve large-scale sequence similarity estimation by mapping sequences to more easily comparable features that can approximate edit distances efficiently. Substrings or k-mers, as the dominant choice of features, face an unavoidable compromise between sensitivity and specificity when selecting the proper k-value. Recently, subsequence-based features have shown improved performance, but they are computationally demanding, and determining the ideal subsequence length remains an intricate art. In this work, we introduce SubseqSketch, a novel alignment-free scheme that maps a sequence to an integer vector, where the entries correspond to dynamic, rather than fixed, lengths of random subsequences. The cosine similarity between these vectors exhibits a strong correlation with the edit similarity between the original sequences. Through experiments on benchmark datasets, we demonstrate that SubseqSketch is both efficient and effective across various alignment-free tasks, including nearest neighbor search and phylogenetic clustering. A C++ implementation of SubseqSketch is openly available at https://github.com/Shao-Group/SubseqSketch.
Cite as

Ke Chen, Vinamratha Pattar, and Mingfu Shao. Sequence Similarity Estimation by Random Subsequence Sketching. In 25th International Conference on Algorithms for Bioinformatics (WABI 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 344, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.WABI.2025.7,
  author =	{Chen, Ke and Pattar, Vinamratha and Shao, Mingfu},
  title =	{{Sequence Similarity Estimation by Random Subsequence Sketching}},
  booktitle =	{25th International Conference on Algorithms for Bioinformatics (WABI 2025)},
  pages =	{7:1--7:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-386-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{344},
  editor =	{Brejov\'{a}, Bro\v{n}a and Patro, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WABI.2025.7},
  URN =		{urn:nbn:de:0030-drops-239332},
  doi =		{10.4230/LIPIcs.WABI.2025.7},
  annote =	{Keywords: Alignment-free sequence comparison, Phylogenetic clustering, Nearest neighbor search, Edit distance embedding}
}
Document
Research
DOI: 10.4230/OASIcs.Grossi.20
Subsequence-Based Indices for Genome Sequence Analysis

Authors: Giovanni Buzzega, Alessio Conte, Veronica Guerrini, Giulia Punzi, Giovanna Rosone, and Lorenzo Tattini

Published in: OASIcs, Volume 132, From Strings to Graphs, and Back Again: A Festschrift for Roberto Grossi's 60th Birthday (2025)

Abstract
Compact indices are a fundamental tool in string analysis, even more so in bioinformatics, where genomic sequences can reach billions in length. This paper presents some recent results in which Roberto Grossi has been involved, showing how some of these indices do more than just efficiently represent data, but rather are able to bring out salient information within it, which can be exploited for their downstream analysis. Specifically, we first review a recently-introduced method [Guerrini et al., 2023] that employs the Burrows-Wheeler Transform to build reasonably accurate phylogenetic trees in an assembly-free scenario. We then describe a recent practical tool [Buzzega et al., 2025] for indexing Maximal Common Subsequences between strings, which can enable analysis of genomic sequence similarity. Experimentally, we show that the results produced by the one index are consistent with the expectations about the results of the other index.
Cite as

Giovanni Buzzega, Alessio Conte, Veronica Guerrini, Giulia Punzi, Giovanna Rosone, and Lorenzo Tattini. Subsequence-Based Indices for Genome Sequence Analysis. In From Strings to Graphs, and Back Again: A Festschrift for Roberto Grossi's 60th Birthday. Open Access Series in Informatics (OASIcs), Volume 132, pp. 20:1-20:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{buzzega_et_al:OASIcs.Grossi.20,
  author =	{Buzzega, Giovanni and Conte, Alessio and Guerrini, Veronica and Punzi, Giulia and Rosone, Giovanna and Tattini, Lorenzo},
  title =	{{Subsequence-Based Indices for Genome Sequence Analysis}},
  booktitle =	{From Strings to Graphs, and Back Again: A Festschrift for Roberto Grossi's 60th Birthday},
  pages =	{20:1--20:21},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-391-1},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{132},
  editor =	{Conte, Alessio and Marino, Andrea and Rosone, Giovanna and Vitter, Jeffrey Scott},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Grossi.20},
  URN =		{urn:nbn:de:0030-drops-238199},
  doi =		{10.4230/OASIcs.Grossi.20},
  annote =	{Keywords: String Indices, Burrows-Wheeler Transform, Maximal Common Subsequences, Sequence Analysis, Phylogeny}
}
Document
DOI: 10.4230/LIPIcs.SAND.2025.12
Restless Exploration and Token Dissemination in Vertex-Permuted Temporal Graphs

Authors: Kamran Ayoubi and Lata Narayanan

Published in: LIPIcs, Volume 330, 4th Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2025)

Abstract
In the temporal graph exploration problem, an agent wishes to visit all the vertices of a temporal graph, moving at most one edge in every time step. In restless exploration, the agent is required to move in every step, and cannot wait at a vertex. We study the problem of restless exploration in vertex-permuted graphs, which are a class of temporal graphs in which the topology of the graph stays the same in every time step. In other words, in a vertex permuted temporal graph, in every step i, the graph G_i is isomorphic to the same base graph G. We give a precise characterization of graphs G such that restless exploration is possible in every vertex-permuted graph with base graph G. Our technique is based on an a characterization of networks in which there is an online distributed algorithm for restless token dissemination. Finally we describe some families of graphs in which restless exploration is always possible, and some in which it is not.
Cite as

Kamran Ayoubi and Lata Narayanan. Restless Exploration and Token Dissemination in Vertex-Permuted Temporal Graphs. In 4th Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 330, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ayoubi_et_al:LIPIcs.SAND.2025.12,
  author =	{Ayoubi, Kamran and Narayanan, Lata},
  title =	{{Restless Exploration and Token Dissemination in Vertex-Permuted Temporal Graphs}},
  booktitle =	{4th Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2025)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-368-3},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{330},
  editor =	{Meeks, Kitty and Scheideler, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAND.2025.12},
  URN =		{urn:nbn:de:0030-drops-230658},
  doi =		{10.4230/LIPIcs.SAND.2025.12},
  annote =	{Keywords: Temporal graphs, Vertex permuted graphs, Restless exploration, Periodic graphs, Token dissemination}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.8
Unsolvability of the Quintic Formalized in Dependent Type Theory

Authors: Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
In this paper, we describe an axiom-free Coq formalization that there does not exists a general method for solving by radicals polynomial equations of degree greater than 4. This development includes a proof of Galois' Theorem of the equivalence between solvable extensions and extensions solvable by radicals. The unsolvability of the general quintic follows from applying this theorem to a well chosen polynomial with unsolvable Galois group.
Cite as

Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub. Unsolvability of the Quintic Formalized in Dependent Type Theory. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bernard_et_al:LIPIcs.ITP.2021.8,
  author =	{Bernard, Sophie and Cohen, Cyril and Mahboubi, Assia and Strub, Pierre-Yves},
  title =	{{Unsolvability of the Quintic Formalized in Dependent Type Theory}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.8},
  URN =		{urn:nbn:de:0030-drops-139038},
  doi =		{10.4230/LIPIcs.ITP.2021.8},
  annote =	{Keywords: Galois theory, Coq, Mathematical Components, Dependent Type Theory, Abel-Ruffini, General quintic}
}
  • Refine by Type
  • 11 Document/PDF
  • 10 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 9 2025
  • 1 2021

  • Refine by Author
  • 1 Avigad, Jeremy
  • 1 Ayoubi, Kamran
  • 1 Bensch, Leonie
  • 1 Bensch, Oliver
  • 1 Bernard, Sophie
  • Show More...

  • Refine by Series/Journal
  • 8 LIPIcs
  • 3 OASIcs

  • Refine by Classification
  • 2 Mathematics of computing → Graph theory
  • 2 Theory of computation → Graph algorithms analysis
  • 2 Theory of computation → Type theory
  • 1 Applied computing → Aerospace
  • 1 Applied computing → Bioinformatics
  • Show More...

  • Refine by Keyword
  • 2 Dependent Type Theory
  • 1 Abel-Ruffini
  • 1 Alignment-free sequence comparison
  • 1 Approximation algorithm
  • 1 Artificial Intelligence
  • 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