10 Search Results for "Chung, Christine"

Document
DOI: 10.4230/LIPIcs.ITCS.2026.54
Testable Algorithms for Approximately Counting Edges and Triangles in Sublinear Time and Space

Authors: Talya Eden, Ronitt Rubinfeld, and Arsen Vasilyan

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract
We consider the fundamental problems of approximately counting the numbers of edges and triangles in a graph in sublinear time. Previous algorithms for these tasks are significantly more efficient under a promise that the arboricity of the graph is bounded by some parameter ̅α. However, when this promise is violated, the estimates given by these algorithms are no longer guaranteed to be correct. For the triangle counting task, we give an algorithm that requires no promise on the input graph G, and computes a (1±ε)-approximation for the number of triangles t in G in time O^*((m⋅ α(G))/t + m/(t^{2/3)}), where α(G) is the arboricity of the graph. The algorithm can be used on any graph G (no prior knowledge of the arboricity α(G) is required), and the algorithm adapts its run-time on the fly based on the graph G. We accomplish this by trying a sequence of candidate values α̃ for α(G) and using a novel algorithm in the framework of testable algorithms. This ensures that wrong candidates α̃ cannot lead to wrong estimates: if the advice is incorrect, the algorithm either succeeds despite this or detects this and continues with a new candidate. Once the algorithm accepts the candidate, its output is guaranteed to be correct with high probability. We prove that this approach preserves - up to an additive overhead - the dramatic efficiency gains obtainable when good arboricity bounds are known in advance, while ensuring robustness against misleading advice. We further complement this result with a lower bound, showing that such an overhead is unavoidable whenever the advice may be faulty. We further demonstrate implications of our results for triangle counting in the streaming model.
Cite as

Talya Eden, Ronitt Rubinfeld, and Arsen Vasilyan. Testable Algorithms for Approximately Counting Edges and Triangles in Sublinear Time and Space. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 54:1-54:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{eden_et_al:LIPIcs.ITCS.2026.54,
  author =	{Eden, Talya and Rubinfeld, Ronitt and Vasilyan, Arsen},
  title =	{{Testable Algorithms for Approximately Counting Edges and Triangles in Sublinear Time and Space}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{54:1--54:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.54},
  URN =		{urn:nbn:de:0030-drops-253417},
  doi =		{10.4230/LIPIcs.ITCS.2026.54},
  annote =	{Keywords: Sublinear Algorithms, Triangle Counting, Edge Counting, Arboricity}
}
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/LIPIcs.ITP.2025.30
Nondeterministic Asynchronous Dataflow in Isabelle/HOL

Authors: Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel

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

Abstract
We formalize nondeterministic asynchronous dataflow networks in Isabelle/HOL. Dataflow networks are comprised of operators that are capable of communicating with the network, performing silent computations, and making nondeterministic choices. We represent operators using a shallow embedding as codatatypes. Using this representation, we define standard asynchronous dataflow primitives, including sequential and parallel composition and a feedback operator. These primitives adhere to a number of laws from the literature, which we prove by coinduction using weak bisimilarity as our equality. Albeit coinductive and nondeterministic, our model is executable via code extraction to Haskell.
Cite as

Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel. Nondeterministic Asynchronous Dataflow in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{silva_et_al:LIPIcs.ITP.2025.30,
  author =	{Silva, Rafael Castro Gon\c{c}alves and Fernet, Laouen and Traytel, Dmitriy},
  title =	{{Nondeterministic Asynchronous Dataflow in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{30:1--30: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.30},
  URN =		{urn:nbn:de:0030-drops-246280},
  doi =		{10.4230/LIPIcs.ITP.2025.30},
  annote =	{Keywords: dataflow, verification, coinduction, Isabelle/HOL}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.94
A Nearly Optimal Deterministic Algorithm for Online Transportation Problem

Authors: Tsubasa Harada and Toshiya Itoh

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

Abstract
For the online transportation problem with m server sites, it has long been known that the competitive ratio of any deterministic algorithm is at least 2m-1. Kalyanasundaram and Pruhs conjectured in 1998 that a deterministic (2m-1)-competitive algorithm exists for this problem, a conjecture that has remained open for over two decades. In this paper, we propose a new deterministic algorithm for the online transportation problem and show that it achieves a competitive ratio of at most 8m-5. This is the first O(m)-competitive deterministic algorithm, coming close to the lower bound of 2m-1 within a constant factor.
Cite as

Tsubasa Harada and Toshiya Itoh. A Nearly Optimal Deterministic Algorithm for Online Transportation Problem. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 94:1-94:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{harada_et_al:LIPIcs.ICALP.2025.94,
  author =	{Harada, Tsubasa and Itoh, Toshiya},
  title =	{{A Nearly Optimal Deterministic Algorithm for Online Transportation Problem}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{94:1--94:17},
  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.94},
  URN =		{urn:nbn:de:0030-drops-234712},
  doi =		{10.4230/LIPIcs.ICALP.2025.94},
  annote =	{Keywords: Online algorithms, Competitive analysis, Online metric matching, Online weighted matching, Online minimum weight perfect matching, Online transportation problem, Online facility assignment, Greedy algorithm}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.12
Automatic Goal Clone Detection in Rocq

Authors: Ali Ghanbari

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

Abstract
Proof engineering in Rocq is a labor-intensive process, and as proof developments grow in size, redundancy and maintainability become challenges. One such redundancy is goal cloning, i.e., proving α-equivalent goals multiple times, leading to wasted effort and bloated proof scripts. In this paper, we introduce clone-finder, a novel technique for detecting goal clones in Rocq proofs. By leveraging the formal notion of α-equivalence for Gallina terms, clone-finder systematically identifies duplicated proof goals across large Rocq codebases. We evaluate clone-finder on 40 real-world Rocq projects from the CoqGym dataset. Our results reveal that each project contains an average of 27.73 instances of goal clone. We observed that the clones can be categorized as either exact goal duplication, generalization, or α-equivalent goals with different proofs, each signifying varying levels duplicate effort. Our findings highlight significant untapped potential for proof reuse in Rocq-based formal verification projects, paving the way for future improvements in automated proof engineering.
Cite as

Ali Ghanbari. Automatic Goal Clone Detection in Rocq. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ghanbari:LIPIcs.ECOOP.2025.12,
  author =	{Ghanbari, Ali},
  title =	{{Automatic Goal Clone Detection in Rocq}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{12:1--12:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.12},
  URN =		{urn:nbn:de:0030-drops-233055},
  doi =		{10.4230/LIPIcs.ECOOP.2025.12},
  annote =	{Keywords: Clone Detection, Goal, Proof, Rocq, Gallina}
}
Document
Short Paper
DOI: 10.4230/OASIcs.ATMOS.2024.8
New Bounds on the Performance of SBP for the Dial-a-Ride Problem with Revenues (Short Paper)

Authors: Barbara M. Anthony, Christine Chung, Ananya Das, and David Yuen

Published in: OASIcs, Volume 123, 24th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2024)

Abstract
We revisit the Segmented Best Path (sbp) algorithm for online DARP in an offline setting with revenues and a time limit. The goal is to find a subset of the inputted ride requests that can be served within the time limit while maximizing the total revenue earned. sbp divides the time into segments and greedily chooses the highest-revenue path of requests to serve within each time segment. We show that sbp’s performance has an upper bound of 5. Further, while sbp is a tight 4-approximation in the uniform-revenue case, we find that with non-uniform revenues, the approximation ratio of sbp has a lower bound strictly greater than 4; in particular, we provide a lower bound of (√e + 1)/(√e - 1) ≈ 4.08299, which we show can be generalized to instances with ratio greater than 4.278.
Cite as

Barbara M. Anthony, Christine Chung, Ananya Das, and David Yuen. New Bounds on the Performance of SBP for the Dial-a-Ride Problem with Revenues (Short Paper). In 24th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2024). Open Access Series in Informatics (OASIcs), Volume 123, pp. 8:1-8:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{anthony_et_al:OASIcs.ATMOS.2024.8,
  author =	{Anthony, Barbara M. and Chung, Christine and Das, Ananya and Yuen, David},
  title =	{{New Bounds on the Performance of SBP for the Dial-a-Ride Problem with Revenues}},
  booktitle =	{24th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2024)},
  pages =	{8:1--8:6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-350-8},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{123},
  editor =	{Bouman, Paul C. and Kontogiannis, Spyros C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2024.8},
  URN =		{urn:nbn:de:0030-drops-211964},
  doi =		{10.4230/OASIcs.ATMOS.2024.8},
  annote =	{Keywords: Dial-a-Ride problems, Lower bounds, Vehicle routing}
}
Document
Position
DOI: 10.4230/TGDK.1.1.5
Knowledge Graphs for the Life Sciences: Recent Developments, Challenges and Opportunities

Authors: Jiaoyan Chen, Hang Dong, Janna Hastings, Ernesto Jiménez-Ruiz, Vanessa López, Pierre Monnin, Catia Pesquita, Petr Škoda, and Valentina Tamma

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
The term life sciences refers to the disciplines that study living organisms and life processes, and include chemistry, biology, medicine, and a range of other related disciplines. Research efforts in life sciences are heavily data-driven, as they produce and consume vast amounts of scientific data, much of which is intrinsically relational and graph-structured. The volume of data and the complexity of scientific concepts and relations referred to therein promote the application of advanced knowledge-driven technologies for managing and interpreting data, with the ultimate aim to advance scientific discovery. In this survey and position paper, we discuss recent developments and advances in the use of graph-based technologies in life sciences and set out a vision for how these technologies will impact these fields into the future. We focus on three broad topics: the construction and management of Knowledge Graphs (KGs), the use of KGs and associated technologies in the discovery of new knowledge, and the use of KGs in artificial intelligence applications to support explanations (explainable AI). We select a few exemplary use cases for each topic, discuss the challenges and open research questions within these topics, and conclude with a perspective and outlook that summarizes the overarching challenges and their potential solutions as a guide for future research.
Cite as

Jiaoyan Chen, Hang Dong, Janna Hastings, Ernesto Jiménez-Ruiz, Vanessa López, Pierre Monnin, Catia Pesquita, Petr Škoda, and Valentina Tamma. Knowledge Graphs for the Life Sciences: Recent Developments, Challenges and Opportunities. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 5:1-5:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{chen_et_al:TGDK.1.1.5,
  author =	{Chen, Jiaoyan and Dong, Hang and Hastings, Janna and Jim\'{e}nez-Ruiz, Ernesto and L\'{o}pez, Vanessa and Monnin, Pierre and Pesquita, Catia and \v{S}koda, Petr and Tamma, Valentina},
  title =	{{Knowledge Graphs for the Life Sciences: Recent Developments, Challenges and Opportunities}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{5:1--5:33},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.5},
  URN =		{urn:nbn:de:0030-drops-194791},
  doi =		{10.4230/TGDK.1.1.5},
  annote =	{Keywords: Knowledge graphs, Life science, Knowledge discovery, Explainable AI}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2019.11
Maximizing the Number of Rides Served for Dial-a-Ride

Authors: Barbara M. Anthony, Ricky Birnbaum, Sara Boyd, Ananya Christman, Christine Chung, Patrick Davis, Jigar Dhimar, and David Yuen

Published in: OASIcs, Volume 75, 19th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2019)

Abstract
We study a variation of offline Dial-a-Ride, where each request has not only a source and destination, but also a revenue that is earned for serving the request. We investigate this problem for the uniform metric space with uniform revenues. While we present a study on a simplified setting of the problem that has limited practical applications, this work provides the theoretical foundation for analyzing the more general forms of the problem. Since revenues are uniform the problem is equivalent to maximizing the number of served requests. We show that the problem is NP-hard and present a 2/3 approximation algorithm. We also show that a natural generalization of this algorithm has an approximation ratio at most 7/9.
Cite as

Barbara M. Anthony, Sara Boyd, Ricky Birnbaum, Ananya Christman, Christine Chung, Patrick Davis, Jigar Dhimar, and David Yuen. Maximizing the Number of Rides Served for Dial-a-Ride. In 19th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2019). Open Access Series in Informatics (OASIcs), Volume 75, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{anthony_et_al:OASIcs.ATMOS.2019.11,
  author =	{Anthony, Barbara M. and Birnbaum, Ricky and Boyd, Sara and Christman, Ananya and Chung, Christine and Davis, Patrick and Dhimar, Jigar and Yuen, David},
  title =	{{Maximizing the Number of Rides Served for Dial-a-Ride}},
  booktitle =	{19th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2019)},
  pages =	{11:1--11:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-128-3},
  ISSN =	{2190-6807},
  year =	{2019},
  volume =	{75},
  editor =	{Cacchiani, Valentina and Marchetti-Spaccamela, Alberto},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2019.11},
  URN =		{urn:nbn:de:0030-drops-114237},
  doi =		{10.4230/OASIcs.ATMOS.2019.11},
  annote =	{Keywords: dial-a-ride, revenue maximization, approximation algorithm, vehicle routing}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2017.1
Revenue Maximization in Online Dial-A-Ride

Authors: Ananya Christman, Christine Chung, Nicholas Jaczko, Marina Milan, Anna Vasilchenko, and Scott Westvold

Published in: OASIcs, Volume 59, 17th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2017)

Abstract
We study a variation of the Online-Dial-a-Ride Problem where each request comes with not only a source, destination and release time, but also has an associated revenue. The server's goal is to maximize its total revenue within a given time limit, T. We show that the competitive ratio is unbounded for any deterministic online algorithm for the problem. We then provide a 3-competitive algorithm for the problem in a uniform metric space and a 6-competitive algorithm for the general case of weighted graphs (under reasonable assumptions about the input instance). We conclude with an experimental evaluation of our algorithm in simulated settings inspired by real-world Dial-a-Ride data. Experimental results show that our algorithm performs well when compared to an offline version of the algorithm and a greedy algorithm.
Cite as

Ananya Christman, Christine Chung, Nicholas Jaczko, Marina Milan, Anna Vasilchenko, and Scott Westvold. Revenue Maximization in Online Dial-A-Ride. In 17th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2017). Open Access Series in Informatics (OASIcs), Volume 59, pp. 1:1-1:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{christman_et_al:OASIcs.ATMOS.2017.1,
  author =	{Christman, Ananya and Chung, Christine and Jaczko, Nicholas and Milan, Marina and Vasilchenko, Anna and Westvold, Scott},
  title =	{{Revenue Maximization in Online Dial-A-Ride}},
  booktitle =	{17th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2017)},
  pages =	{1:1--1:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-042-2},
  ISSN =	{2190-6807},
  year =	{2017},
  volume =	{59},
  editor =	{D'Angelo, Gianlorenzo and Dollevoet, Twan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2017.1},
  URN =		{urn:nbn:de:0030-drops-78886},
  doi =		{10.4230/OASIcs.ATMOS.2017.1},
  annote =	{Keywords: online algorithms, dial-a-ride, competitive analysis, vehicle routing, metric space}
}
Document
DOI: 10.4230/LITES-v003-i001-a005
A Survey on Static Cache Analysis for Real-Time Systems

Authors: Mingsong Lv, Nan Guan, Jan Reineke, Reinhard Wilhelm, and Wang Yi

Published in: LITES, Volume 3, Issue 1 (2016). Leibniz Transactions on Embedded Systems, Volume 3, Issue 1

Abstract
Real-time systems are reactive computer systems that must produce their reaction to a stimulus within given time bounds. A vital verification requirement is to estimate the Worst-Case Execution Time (WCET) of programs. These estimates are then used to predict the timing behavior of the overall system. The execution time of a program heavily depends on the underlying hardware, among which cache has the biggest influence. Analyzing cache behavior is very challenging due to the versatile cache features and complex execution environment. This article provides a survey on static cache analysis for real-time systems. We first present the challenges and static analysis techniques for independent programs with respect to different cache features. Then, the discussion is extended to cache analysis in complex execution environment, followed by a survey of existing tools based on static techniques for cache analysis. An outlook for future research is provided at last.
Cite as

Mingsong Lv, Nan Guan, Jan Reineke, Reinhard Wilhelm, and Wang Yi. A Survey on Static Cache Analysis for Real-Time Systems. In LITES, Volume 3, Issue 1 (2016). Leibniz Transactions on Embedded Systems, Volume 3, Issue 1, pp. 05:1-05:48, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{lv_et_al:LITES-v003-i001-a005,
  author =	{Lv, Mingsong and Guan, Nan and Reineke, Jan and Wilhelm, Reinhard and Yi, Wang},
  title =	{{A Survey on Static Cache Analysis for Real-Time Systems}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{05:1--05:48},
  ISSN =	{2199-2002},
  year =	{2016},
  volume =	{3},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v003-i001-a005},
  URN =		{urn:nbn:de:0030-drops-192603},
  doi =		{10.4230/LITES-v003-i001-a005},
  annote =	{Keywords: Hard real-time, Cache analysis, Worst-case execution time}
}
  • Refine by Type
  • 10 Document/PDF
  • 6 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 4 2025
  • 1 2024
  • 1 2023
  • 1 2019
  • Show More...

  • Refine by Author
  • 3 Chung, Christine
  • 2 Anthony, Barbara M.
  • 2 Christman, Ananya
  • 2 Yuen, David
  • 1 Bernstein, Abraham
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs
  • 3 OASIcs
  • 1 LITES
  • 2 TGDK

  • Refine by Classification
  • 2 Information systems → Graph-based database models
  • 2 Theory of computation → Routing and network design problems
  • 1 Applied computing → Life and medical sciences
  • 1 Applied computing → Transportation
  • 1 Computing methodologies → Distributed algorithms
  • Show More...

  • Refine by Keyword
  • 2 dial-a-ride
  • 2 vehicle routing
  • 1 Arboricity
  • 1 Argument Mining
  • 1 Cache analysis
  • 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