12 Search Results for "Anderson, Taylor"

Document
DOI: 10.4230/LIPIcs.SEA.2026.20
QuadRank: Engineering a High Throughput Rank

Authors: Ragnar Groot Koerkamp

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

Abstract
Motivation. Given a text, a query rank(q, c) counts the number of occurrences of character c among the first q characters of the text. Space-efficient methods to answer these rank queries form an important building block in many succinct data structures. For example, the FM-index [Ferragina and Manzini, 2000] is a widely used data structure that uses rank queries to locate all occurrences of a pattern in a text. In bioinformatics applications, the goal is usually to process large inputs as fast as possible. Thus, data structures should have high throughput when used with many threads. Contributions. We first survey existing results on rank data structures. For the σ = 2 binary alphabet, we then develop BiRank, which has 3.28% space overhead. BiRank merges the central ideas of two recent papers: (1) we interleave (inline) offsets in each cache line of the underlying bit vector [Laws et al., 2024], reducing cache misses, and (2) these offsets are to the middle of each block so that only half of each needs popcounting [Gottlieb and Reinert, 2025]. In QuadRank (14.4% overhead), we extend these techniques to the σ = 4 (DNA) alphabet. Both data structures typically require only a single cache miss per query, making them highly suitable for high-throughput and memory-bound settings. To enable efficient batch-processing, we support prefetching the cache lines required to answer upcoming queries. Results. BiRank and QuadRank are around 1.5× and 2× faster than similar-overhead methods that do not use interleaving. Prefetching gives an additional 2× speedup, at which point the dual-channel DDR4 RAM bandwidth becomes a hard limit on the total throughput. With prefetching, both methods outperform all other methods apart from SPIDER [Laws et al., 2024] by 2×. When using QuadRank with prefetching in a toy count-only FM-index, QuadFm, this results in a smaller size and up to 4× speedup over Genedex, a state-of-the-art batching FM-index implementation. Conclusion. Optimizing data structures for high throughput, by minimizing cache misses and branch-misses and adding support for prefetching, can result in significant speedups when benchmarks are adjusted accordingly.
Cite as

Ragnar Groot Koerkamp. QuadRank: Engineering a High Throughput Rank. In 24th International Symposium on Experimental Algorithms (SEA 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 371, pp. 20:1-20:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{grootkoerkamp:LIPIcs.SEA.2026.20,
  author =	{Groot Koerkamp, Ragnar},
  title =	{{QuadRank: Engineering a High Throughput Rank}},
  booktitle =	{24th International Symposium on Experimental Algorithms (SEA 2026)},
  pages =	{20:1--20:23},
  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.20},
  URN =		{urn:nbn:de:0030-drops-260248},
  doi =		{10.4230/LIPIcs.SEA.2026.20},
  annote =	{Keywords: Rank, Succinct Data Structures, Cache Performance, Prefetching}
}
Document
Research
DOI: 10.4230/TGDK.3.3.4
Mining Inter-Document Argument Structures in Scientific Papers for an Argument Web

Authors: Florian Ruosch, Cristina Sarasua, and Abraham Bernstein

Published in: TGDK, Volume 3, Issue 3 (2025). Transactions on Graph Data and Knowledge, Volume 3, Issue 3

Abstract
In Argument Mining, predicting argumentative relations between texts (or spans) remains one of the most challenging aspects, even more so in the cross-document setting. This paper makes three key contributions to advance research in this domain. We first extend an existing dataset, the Sci-Arg corpus, by annotating it with explicit inter-document argumentative relations, thereby allowing arguments to be distributed over several documents forming an Argument Web; these new annotations are published using Semantic Web technologies (RDF, OWL). Second, we explore and evaluate three automated approaches for predicting these inter-document argumentative relations, establishing critical baselines on the new dataset. We find that a simple classifier based on discourse indicators with access to context outperforms neural methods. Third, we conduct a comparative analysis of these approaches for both intra- and inter-document settings, identifying statistically significant differences in results that indicate the necessity of distinguishing between these two scenarios. Our findings highlight significant challenges in this complex domain and open crucial avenues for future research on the Argument Web of Science, particularly for those interested in leveraging Semantic Web technologies and knowledge graphs to understand scholarly discourse. With this, we provide the first stepping stones in the form of a benchmark dataset, three baseline methods, and an initial analysis for a systematic exploration of this field relevant to the Web of Data and Science.
Cite as

Florian Ruosch, Cristina Sarasua, and Abraham Bernstein. Mining Inter-Document Argument Structures in Scientific Papers for an Argument Web. In Transactions on Graph Data and Knowledge (TGDK), Volume 3, Issue 3, pp. 4:1-4:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{ruosch_et_al:TGDK.3.3.4,
  author =	{Ruosch, Florian and Sarasua, Cristina and Bernstein, Abraham},
  title =	{{Mining Inter-Document Argument Structures in Scientific Papers for an Argument Web}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{4:1--4:33},
  ISSN =	{2942-7517},
  year =	{2025},
  volume =	{3},
  number =	{3},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.3.3.4},
  URN =		{urn:nbn:de:0030-drops-252159},
  doi =		{10.4230/TGDK.3.3.4},
  annote =	{Keywords: Argument Mining, Large Language Models, Knowledge Graphs, Link Prediction}
}
Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.3
Multidimensional Usability Assessment in Spaceflight Analog Missions

Authors: Shivang Shelat, Katherine E. Homer, John A. Karasinski, and Jessica J. Marquez

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

Abstract
Software planning tools enable the self-scheduling of operational timelines during spaceflight, reducing reliance on ground support crews. Here, we assess analog crew perceptions of a planning tool’s usability across two space mission analogs with two validated questionnaires: the unidimensional System Usability Scale and the multidimensional User Experience Questionnaire. Critically, half the missions had assistive countermeasures integrated into the planning software interface whereas the other half did not. Correlation tests revealed high convergence between usability measures in the spaceflight analog setting. Group comparisons showed that the interface countermeasures enhanced several dimensions of usability, particularly for perceptions of the tool’s efficiency and dependability. These findings highlight the utility of a multidimensional approach to characterizing usability in order to capture fine-grained shifts in human-software dynamics, especially in spaceflight environments.
Cite as

Shivang Shelat, Katherine E. Homer, John A. Karasinski, and Jessica J. Marquez. Multidimensional Usability Assessment in Spaceflight Analog Missions. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 3:1-3:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{shelat_et_al:OASIcs.SpaceCHI.2025.3,
  author =	{Shelat, Shivang and Homer, Katherine E. and Karasinski, John A. and Marquez, Jessica J.},
  title =	{{Multidimensional Usability Assessment in Spaceflight Analog Missions}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{3:1--3:9},
  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.3},
  URN =		{urn:nbn:de:0030-drops-239934},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.3},
  annote =	{Keywords: space usability, crew autonomy, self-scheduling software}
}
Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.21
Towards Passively Actuated Short-Range Telehaptics for Astronauts

Authors: Matvey Boguslavskiy, Digby Chappell, and Thrishantha Nanayakkara

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

Abstract
Human extra-vehicular activity (EVA) plays a vital role in current and near future space exploration for two reasons: the superior dexterity exhibited by human astronauts, and their flexible problem-solving and decision-making capabilities. However, the dexterity of astronauts during EVA is limited by the flexibility and tactility of their EVA suit gloves, which are primarily designed to provide thermal insulation and pressure for the hand. This creates a compromise between utility and protection. To address this compromise, a Passively Actuated Short-range Telehaptic (PAST) device is proposed. The PAST device couples the motion of fingers between a robotic hand and a human hand through a hydraulically actuated linkage. It also transfers tactile information, including pressure, direction of motion, and position of contact, via a taxel array. Results demonstrate that the proposed prototype PAST device surpasses an unpressurised benchmark heavy work glove (HWG) in tasks involving tactile position and motion direction identification. This provides evidence supporting the feasibility of enhancing astronaut dexterity during EVA through the use of PAST devices as an alternative paradigm to gloves.
Cite as

Matvey Boguslavskiy, Digby Chappell, and Thrishantha Nanayakkara. Towards Passively Actuated Short-Range Telehaptics for Astronauts. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{boguslavskiy_et_al:OASIcs.SpaceCHI.2025.21,
  author =	{Boguslavskiy, Matvey and Chappell, Digby and Nanayakkara, Thrishantha},
  title =	{{Towards Passively Actuated Short-Range Telehaptics for Astronauts}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{21:1--21:16},
  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.21},
  URN =		{urn:nbn:de:0030-drops-240115},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.21},
  annote =	{Keywords: Extra-vehicular Activity, Mechanism Design, Haptics, Dexterity, Tactility}
}
Document
DOI: 10.4230/LIPIcs.WABI.2025.11
Mutational Signature Refitting on Sparse Pan-Cancer Data

Authors: Gal Gilad, Teresa M. Przytycka, and Roded Sharan

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

Abstract
Mutational processes shape cancer genomes, leaving characteristic marks that are termed signatures. The level of activity of each such process, or its signature exposure, provides important information on the disease, improving patient stratification and the prediction of drug response. Thus, there is growing interest in developing refitting methods that decipher those exposures. Previous work in this domain was unsupervised in nature, employing algebraic decomposition and probabilistic inference methods. Here we provide a supervised approach to the problem of signature refitting and show its superiority over current methods. Our method, SuRe, leverages a neural network model to capture correlations between signature exposures in real data. We show that SuRe outperforms previous methods on sparse mutation data from tumor type specific data sets, as well as pan-cancer data sets, with an increasing advantage as the data become sparser. We further demonstrate its utility in clinical settings.
Cite as

Gal Gilad, Teresa M. Przytycka, and Roded Sharan. Mutational Signature Refitting on Sparse Pan-Cancer Data. In 25th International Conference on Algorithms for Bioinformatics (WABI 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 344, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gilad_et_al:LIPIcs.WABI.2025.11,
  author =	{Gilad, Gal and Przytycka, Teresa M. and Sharan, Roded},
  title =	{{Mutational Signature Refitting on Sparse Pan-Cancer Data}},
  booktitle =	{25th International Conference on Algorithms for Bioinformatics (WABI 2025)},
  pages =	{11:1--11:23},
  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.11},
  URN =		{urn:nbn:de:0030-drops-239374},
  doi =		{10.4230/LIPIcs.WABI.2025.11},
  annote =	{Keywords: mutational signatures, signature refitting, cancer genomics, genomic data analysis, somatic mutations}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2025.2
Multi-Objective Memory Bandwidth Regulation and Cache Partitioning for Multicore Real-Time Systems

Authors: Binqi Sun, Zhihang Wei, Andrea Bastoni, Debayan Roy, Mirco Theile, Tomasz Kloda, Rodolfo Pellizzoni, and Marco Caccamo

Published in: LIPIcs, Volume 335, 37th Euromicro Conference on Real-Time Systems (ECRTS 2025)

Abstract
Memory bandwidth regulation and cache partitioning are widely used techniques for achieving predictable timing in real-time computing systems. Combined with partitioned scheduling, these methods require careful co-allocation of tasks and resources to cores, as task execution times strongly depend on available allocated resources. To address this challenge, this paper presents a 0-1 linear program for task-resource co-allocation, along with a multi-objective heuristic designed to minimize resource usage while guaranteeing schedulability under a preemptive EDF scheduling policy. Our heuristic employs a multi-layer framework, where an outer layer explores resource allocations using Pareto-pruned search, and an inner layer optimizes task allocation by solving a knapsack problem using dynamic programming. To evaluate the performance of the proposed optimization algorithm, we profile real-world benchmarks on an embedded AMD UltraScale+ ZCU102 platform, with fine-grained resource partitioning enabled by the Jailhouse hypervisor, leveraging cache set partitioning and MemGuard for memory bandwidth regulation. Experiments based on the benchmarking results show that the proposed 0-1 linear program outperforms existing mixed-integer programs by finding more optimal solutions within the same time limit. Moreover, the proposed multi-objective multi-layer heuristic performs consistently better than the state-of-the-art multi-resource-task co-allocation algorithm in terms of schedulability, resource usage, number of non-dominated solutions, and computational efficiency.
Cite as

Binqi Sun, Zhihang Wei, Andrea Bastoni, Debayan Roy, Mirco Theile, Tomasz Kloda, Rodolfo Pellizzoni, and Marco Caccamo. Multi-Objective Memory Bandwidth Regulation and Cache Partitioning for Multicore Real-Time Systems. In 37th Euromicro Conference on Real-Time Systems (ECRTS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 335, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{sun_et_al:LIPIcs.ECRTS.2025.2,
  author =	{Sun, Binqi and Wei, Zhihang and Bastoni, Andrea and Roy, Debayan and Theile, Mirco and Kloda, Tomasz and Pellizzoni, Rodolfo and Caccamo, Marco},
  title =	{{Multi-Objective Memory Bandwidth Regulation and Cache Partitioning for Multicore Real-Time Systems}},
  booktitle =	{37th Euromicro Conference on Real-Time Systems (ECRTS 2025)},
  pages =	{2:1--2:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-377-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{335},
  editor =	{Mancuso, Renato},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2025.2},
  URN =		{urn:nbn:de:0030-drops-235807},
  doi =		{10.4230/LIPIcs.ECRTS.2025.2},
  annote =	{Keywords: Multi-objective optimization, memory bandwidth regulation, cache partitioning, partitioned scheduling, real-time systems}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2025.9
DAMA: A Dual Arbitration Mechanism for Mixed-Criticality Applications

Authors: Wafic Lawand and Rodolfo Pellizzoni

Published in: LIPIcs, Volume 335, 37th Euromicro Conference on Real-Time Systems (ECRTS 2025)

Abstract
We discuss hardware resource management in mixed-criticality systems, where requestors may issue latency-critical (LTC) and non-latency-critical (NLTC) requests. LTC requests must adhere to strict latency bounds imposed by safety-critical applications, but timely servicing NLTC requests is necessary to maximize overall system performance in the average case. In this paper, we address this tradeoff for a shared memory resource by proposing DAMA, a dual arbitration mechanism that imposes an upper bound on the cumulative latency of LTC requests without unduly impacting NLTC performance. DAMA comprises a high-performance arbiter, a real-time arbiter, and a mechanism that constantly monitors the cumulative latency of requests suffered by each requestor. DAMA primarily executes in high-performance mode and only switches to real-time mode in the rare instances when its incorporated mechanism detects a violation of a task’s timing guarantee. We demonstrate the effectiveness of our arbitration scheme by adapting a predictable prefetcher that issues NLTC requests and attaching it to the L1 caches of our cores. We show both formally and experimentally that DAMA provides timing guarantees for LTC requests while processing other NLTC requests. We also demonstrate that with a negligible overhead of less than 1.5% on the cumulative latency bound of LTC requests, DAMA can achieve an equivalent average performance to a prefetcher that processes requests under a high-performance arbitration scheme.
Cite as

Wafic Lawand and Rodolfo Pellizzoni. DAMA: A Dual Arbitration Mechanism for Mixed-Criticality Applications. In 37th Euromicro Conference on Real-Time Systems (ECRTS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 335, pp. 9:1-9:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lawand_et_al:LIPIcs.ECRTS.2025.9,
  author =	{Lawand, Wafic and Pellizzoni, Rodolfo},
  title =	{{DAMA: A Dual Arbitration Mechanism for Mixed-Criticality Applications}},
  booktitle =	{37th Euromicro Conference on Real-Time Systems (ECRTS 2025)},
  pages =	{9:1--9:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-377-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{335},
  editor =	{Mancuso, Renato},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2025.9},
  URN =		{urn:nbn:de:0030-drops-235875},
  doi =		{10.4230/LIPIcs.ECRTS.2025.9},
  annote =	{Keywords: Real-time Systems, Mixed-criticality Applications, Memory controllers, Prefetchers}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.102
Fourier Analysis of Iterative Algorithms

Authors: Chris Jones and Lucas Pesenti

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

Abstract
We study a general class of nonlinear iterative algorithms which includes power iteration, belief propagation and approximate message passing, and many forms of gradient descent. When the input is a random matrix with i.i.d. entries, we use Boolean Fourier analysis to analyze these algorithms as low-degree polynomials in the entries of the input matrix. Each symmetrized Fourier character represents all monomials with a certain shape as specified by a small graph, which we call a Fourier diagram. We prove fundamental asymptotic properties of the Fourier diagrams: over the randomness of the input, all diagrams with cycles are negligible; the tree-shaped diagrams form a basis of asymptotically independent Gaussian vectors; and, when restricted to the trees, iterative algorithms exactly follow an idealized Gaussian dynamic. We use this to prove a state evolution formula, giving a "complete" asymptotic description of the algorithm’s trajectory. The restriction to tree-shaped monomials mirrors the assumption of the cavity method, a 40-year-old non-rigorous technique in statistical physics which has served as one of the most important techniques in the field. We demonstrate how to implement cavity method derivations by 1) restricting the iteration to its tree approximation, and 2) observing that heuristic cavity method-type arguments hold rigorously on the simplified iteration. Our proofs use combinatorial arguments similar to the trace method from random matrix theory. Finally, we push the diagram analysis to a number of iterations that scales with the dimension n of the input matrix, proving that the tree approximation still holds for a simple variant of power iteration all the way up to n^{Ω(1)} iterations.
Cite as

Chris Jones and Lucas Pesenti. Fourier Analysis of Iterative Algorithms. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 102:1-102:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jones_et_al:LIPIcs.ICALP.2025.102,
  author =	{Jones, Chris and Pesenti, Lucas},
  title =	{{Fourier Analysis of Iterative Algorithms}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{102:1--102:21},
  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.102},
  URN =		{urn:nbn:de:0030-drops-234791},
  doi =		{10.4230/LIPIcs.ICALP.2025.102},
  annote =	{Keywords: Iterative Algorithms, Message-passing Algorithms, Random Matrix Theory}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.36
Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees

Authors: Guanqin Zhang, Kota Fukuda, Zhenya Zhang, H.M.N. Dilum Bandara, Shiping Chen, Jianjun Zhao, and Yulei Sui

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

Abstract
The vulnerability of neural networks to adversarial perturbations has necessitated formal verification techniques that can rigorously certify the quality of neural networks. As the state-of-the-art, branch-and-bound (BaB) is a "divide-and-conquer" strategy that applies off-the-shelf verifiers to sub-problems for which they perform better. While BaB can identify the sub-problems that are necessary to be split, it explores the space of these sub-problems in a naive "first-come-first-served" manner, thereby suffering from an issue of inefficiency to reach a verification conclusion. To bridge this gap, we introduce an order over different sub-problems produced by BaB, concerning with their different likelihoods of containing counterexamples. Based on this order, we propose a novel verification framework Oliva that explores the sub-problem space by prioritizing those sub-problems that are more likely to find counterexamples, in order to efficiently reach the conclusion of the verification. Even if no counterexample can be found in any sub-problem, it only changes the order of visiting different sub-problems and so will not lead to a performance degradation. Specifically, Oliva has two variants, including Oliva^GR, a greedy strategy that always prioritizes the sub-problems that are more likely to find counterexamples, and Oliva^SA, a balanced strategy inspired by simulated annealing that gradually shifts from exploration to exploitation to locate the globally optimal sub-problems. We experimentally evaluate the performance of Oliva on 690 verification problems spanning over 5 models with datasets MNIST and CIFAR-10. Compared to the state-of-the-art approaches, we demonstrate the speedup of Oliva for up to 25× in MNIST, and up to 80× in CIFAR-10.
Cite as

Guanqin Zhang, Kota Fukuda, Zhenya Zhang, H.M.N. Dilum Bandara, Shiping Chen, Jianjun Zhao, and Yulei Sui. Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 36:1-36:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.ECOOP.2025.36,
  author =	{Zhang, Guanqin and Fukuda, Kota and Zhang, Zhenya and Bandara, H.M.N. Dilum and Chen, Shiping and Zhao, Jianjun and Sui, Yulei},
  title =	{{Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{36:1--36:29},
  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.36},
  URN =		{urn:nbn:de:0030-drops-233281},
  doi =		{10.4230/LIPIcs.ECOOP.2025.36},
  annote =	{Keywords: neural network verification, branch and bound, counterexample potentiality, simulated annealing, stochastic optimization}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.GIScience.2023.76
A Data-Driven Decision-Making Framework for Spatial Agent-Based Models of Infectious Disease Spread (Short Paper)

Authors: Emma Von Hoene, Amira Roess, and Taylor Anderson

Published in: LIPIcs, Volume 277, 12th International Conference on Geographic Information Science (GIScience 2023)

Abstract
Agent-based models (ABMs) are powerful tools used for better understanding, predicting, and responding to diseases. ABMs are well-suited to represent human health behaviors, a key driver of disease spread. However, many existing ABMs of infectious respiratory disease spread oversimplify or ignore behavioral aspects due to limited data and the variety of behavioral theories available. Therefore, this study aims to develop and implement a data-driven framework for agent decision-making related to health behaviors in geospatial ABMs of infectious disease spread. The agent decision-making framework uses a logistic regression model expressed in the form of odds ratios to calculate the probability of adopting a behavior. The framework is integrated into a geospatial ABM that simulates the spread of COVID-19 and mask usage among the student population at George Mason University in Fall 2021. The framework leverages odds ratios, which can be derived from surveys or open data, and can be modified to incorporate variables identified by behavioral theories. This advancement will offer the public and decision-makers greater insight into disease transmission, accurate predictions on disease outcomes, and preparation for future infectious disease outbreaks.
Cite as

Emma Von Hoene, Amira Roess, and Taylor Anderson. A Data-Driven Decision-Making Framework for Spatial Agent-Based Models of Infectious Disease Spread (Short Paper). In 12th International Conference on Geographic Information Science (GIScience 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 277, pp. 76:1-76:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{vonhoene_et_al:LIPIcs.GIScience.2023.76,
  author =	{Von Hoene, Emma and Roess, Amira and Anderson, Taylor},
  title =	{{A Data-Driven Decision-Making Framework for Spatial Agent-Based Models of Infectious Disease Spread}},
  booktitle =	{12th International Conference on Geographic Information Science (GIScience 2023)},
  pages =	{76:1--76:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-288-4},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{277},
  editor =	{Beecham, Roger and Long, Jed A. and Smith, Dianna and Zhao, Qunshan and Wise, Sarah},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.GIScience.2023.76},
  URN =		{urn:nbn:de:0030-drops-189712},
  doi =		{10.4230/LIPIcs.GIScience.2023.76},
  annote =	{Keywords: Agent-based model, geographic information science, disease simulation, COVID-19, agent behavior, mask use}
}
Document
DOI: 10.4230/DagRep.12.1.1
Mobility Data Science (Dagstuhl Seminar 22021)

Authors: Mohamed Mokbel, Mahmoud Sakr, Li Xiong, Andreas Züfle, Jussara Almeida, Taylor Anderson, Walid Aref, Gennady Andrienko, Natalia Andrienko, Yang Cao, Sanjay Chawla, Reynold Cheng, Panos Chrysanthis, Xiqi Fei, Gabriel Ghinita, Anita Graser, Dimitrios Gunopulos, Christian Jensen, Joon-Sook Kim, Kyoung-Sook Kim, Peer Kröger, John Krumm, Johannes Lauer, Amr Magdy, Mario Nascimento, Siva Ravada, Matthias Renz, Dimitris Sacharidis, Cyrus Shahabi, Flora Salim, Mohamed Sarwat, Maxime Schoemans, Bettina Speckmann, Egemen Tanin, Yannis Theodoridis, Kristian Torp, Goce Trajcevski, Marc van Kreveld, Carola Wenk, Martin Werner, Raymond Wong, Song Wu, Jianqiu Xu, Moustafa Youssef, Demetris Zeinalipour, Mengxuan Zhang, and Esteban Zimányi

Published in: Dagstuhl Reports, Volume 12, Issue 1 (2022)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 22021 "Mobility Data Science". This seminar was held January 9-14, 2022, including 47 participants from industry and academia. The goal of this Dagstuhl Seminar was to create a new research community of mobility data science in which the whole is greater than the sum of its parts by bringing together established leaders as well as promising young researchers from all fields related to mobility data science. Specifically, this report summarizes the main results of the seminar by (1) defining Mobility Data Science as a research domain, (2) by sketching its agenda in the coming years, and by (3) building a mobility data science community. (1) Mobility data science is defined as spatiotemporal data that additionally captures the behavior of moving entities (human, vehicle, animal, etc.). To understand, explain, and predict behavior, we note that a strong collaboration with research in behavioral and social sciences is needed. (2) Future research directions for mobility data science described in this report include a) mobility data acquisition and privacy, b) mobility data management and analysis, and c) applications of mobility data science. (3) We identify opportunities towards building a mobility data science community, towards collaborations between academic and industry, and towards a mobility data science curriculum.
Cite as

Mohamed Mokbel, Mahmoud Sakr, Li Xiong, Andreas Züfle, Jussara Almeida, Taylor Anderson, Walid Aref, Gennady Andrienko, Natalia Andrienko, Yang Cao, Sanjay Chawla, Reynold Cheng, Panos Chrysanthis, Xiqi Fei, Gabriel Ghinita, Anita Graser, Dimitrios Gunopulos, Christian Jensen, Joon-Sook Kim, Kyoung-Sook Kim, Peer Kröger, John Krumm, Johannes Lauer, Amr Magdy, Mario Nascimento, Siva Ravada, Matthias Renz, Dimitris Sacharidis, Cyrus Shahabi, Flora Salim, Mohamed Sarwat, Maxime Schoemans, Bettina Speckmann, Egemen Tanin, Yannis Theodoridis, Kristian Torp, Goce Trajcevski, Marc van Kreveld, Carola Wenk, Martin Werner, Raymond Wong, Song Wu, Jianqiu Xu, Moustafa Youssef, Demetris Zeinalipour, Mengxuan Zhang, and Esteban Zimányi. Mobility Data Science (Dagstuhl Seminar 22021). In Dagstuhl Reports, Volume 12, Issue 1, pp. 1-34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{mokbel_et_al:DagRep.12.1.1,
  author =	{Mokbel, Mohamed and Sakr, Mahmoud and Xiong, Li and Z\"{u}fle, Andreas and Almeida, Jussara and Anderson, Taylor and Aref, Walid and Andrienko, Gennady and Andrienko, Natalia and Cao, Yang and Chawla, Sanjay and Cheng, Reynold and Chrysanthis, Panos and Fei, Xiqi and Ghinita, Gabriel and Graser, Anita and Gunopulos, Dimitrios and Jensen, Christian and Kim, Joon-Sook and Kim, Kyoung-Sook and Kr\"{o}ger, Peer and Krumm, John and Lauer, Johannes and Magdy, Amr and Nascimento, Mario and Ravada, Siva and Renz, Matthias and Sacharidis, Dimitris and Shahabi, Cyrus and Salim, Flora and Sarwat, Mohamed and Schoemans, Maxime and Speckmann, Bettina and Tanin, Egemen and Theodoridis, Yannis and Torp, Kristian and Trajcevski, Goce and van Kreveld, Marc and Wenk, Carola and Werner, Martin and Wong, Raymond and Wu, Song and Xu, Jianqiu and Youssef, Moustafa and Zeinalipour, Demetris and Zhang, Mengxuan and Zim\'{a}nyi, Esteban},
  title =	{{Mobility Data Science (Dagstuhl Seminar 22021)}},
  pages =	{1--34},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{12},
  number =	{1},
  editor =	{Mokbel, Mohamed and Sakr, Mahmoud and Xiong, Li and Z\"{u}fle, Andreas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.1.1},
  URN =		{urn:nbn:de:0030-drops-169190},
  doi =		{10.4230/DagRep.12.1.1},
  annote =	{Keywords: Spatio-temporal, Tracking, Privacy, Behavior, Data cleaning, Data management, Analytics}
}
Document
DOI: 10.4230/DagSemProc.07461.7
From Algebraic Riccati equations to unilateral quadratic matrix equations: old and new algorithms

Authors: Dario A. Bini, Beatrice Meini, and Federico Poloni

Published in: Dagstuhl Seminar Proceedings, Volume 7461, Numerical Methods for Structured Markov Chains (2008)

Abstract
The problem of reducing an algebraic Riccati equation $XCX-AX-XD+B=0$ to a unilateral quadratic matrix equation (UQME) of the kind $PX^2+QX+R$ is analyzed. New reductions are introduced which enable one to prove some theoretical and computational properties. In particular we show that the structure preserving doubling algorithm of B.D.O. Anderson [Internat. J. Control, 1978] is nothing else but the cyclic reduction algorithm applied to a suitable UQME. A new algorithm obtained by complementing our reductions with the shrink-and-shift tech- nique of Ramaswami is presented. Finally, faster algorithms which require some non-singularity conditions, are designed. The non-singularity re- striction is relaxed by introducing a suitable similarity transformation of the Hamiltonian.
Cite as

Dario A. Bini, Beatrice Meini, and Federico Poloni. From Algebraic Riccati equations to unilateral quadratic matrix equations: old and new algorithms. In Numerical Methods for Structured Markov Chains. Dagstuhl Seminar Proceedings, Volume 7461, pp. 1-28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{bini_et_al:DagSemProc.07461.7,
  author =	{Bini, Dario A. and Meini, Beatrice and Poloni, Federico},
  title =	{{From Algebraic Riccati equations to unilateral quadratic matrix equations: old and new algorithms}},
  booktitle =	{Numerical Methods for Structured Markov Chains},
  pages =	{1--28},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7461},
  editor =	{Dario Bini and Beatrice Meini and Vaidyanathan Ramaswami and Marie-Ange Remiche and Peter Taylor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07461.7},
  URN =		{urn:nbn:de:0030-drops-13987},
  doi =		{10.4230/DagSemProc.07461.7},
  annote =	{Keywords: Algebraic Riccati Equation, Matrix Equation, Cyclic Reduction, Structured doubling algorithm}
}
  • Refine by Type
  • 12 Document/PDF
  • 10 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 8 2025
  • 1 2023
  • 1 2022
  • 1 2008

  • Refine by Author
  • 2 Anderson, Taylor
  • 2 Pellizzoni, Rodolfo
  • 1 Almeida, Jussara
  • 1 Andrienko, Gennady
  • 1 Andrienko, Natalia
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs
  • 2 OASIcs
  • 1 TGDK
  • 1 DagRep
  • 1 DagSemProc

  • Refine by Classification
  • 1 Applied computing → Bioinformatics
  • 1 Computer systems organization → Embedded software
  • 1 Computer systems organization → Real-time system architecture
  • 1 Computer systems organization → Real-time systems
  • 1 Computer systems organization → Robotic control
  • Show More...

  • Refine by Keyword
  • 1 Agent-based model
  • 1 Algebraic Riccati Equation
  • 1 Analytics
  • 1 Argument Mining
  • 1 Behavior
  • 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