9 Search Results for "Edelkamp, Stefan"


Document
Invited Talk
Algorithm Engineering for Sorting and Searching, and All That (Invited Talk)

Authors: Stefan Edelkamp

Published in: LIPIcs, Volume 160, 18th International Symposium on Experimental Algorithms (SEA 2020)


Abstract
We look at several proposals to engineer the set of fundamental searching and sorting algorithms. Aspects are improving locality of disk access and cache access, the efficiency tuning by reducing the number of branch mispredictions, and reducing at leading factors hidden in the Big-Oh notation. These studies in algorithm engineering, in turn, lead to exiting new algorithm designs. On the practical side, we will establish that efficient sorting and searching algorithms are in tight collaboration, as sorting is used for finding duplicates in disk-based search, and heap structures designed for efficient graph search can be exploited in classical and adaptive sorting. We indicate the effects of engineered sorting and searching for combined task and motion planning.

Cite as

Stefan Edelkamp. Algorithm Engineering for Sorting and Searching, and All That (Invited Talk). In 18th International Symposium on Experimental Algorithms (SEA 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 160, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{edelkamp:LIPIcs.SEA.2020.2,
  author =	{Edelkamp, Stefan},
  title =	{{Algorithm Engineering for Sorting and Searching, and All That}},
  booktitle =	{18th International Symposium on Experimental Algorithms (SEA 2020)},
  pages =	{2:1--2:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-148-1},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{160},
  editor =	{Faro, Simone and Cantone, Domenico},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2020.2},
  URN =		{urn:nbn:de:0030-drops-120766},
  doi =		{10.4230/LIPIcs.SEA.2020.2},
  annote =	{Keywords: Sorting, Searching, Algorithm Engineering}
}
Document
BlockQuicksort: Avoiding Branch Mispredictions in Quicksort

Authors: Stefan Edelkamp and Armin Weiss

Published in: LIPIcs, Volume 57, 24th Annual European Symposium on Algorithms (ESA 2016)


Abstract
Since the work of Kaligosi and Sanders (2006), it is well-known that Quicksort - which is commonly considered as one of the fastest in-place sorting algorithms - suffers in an essential way from branch mispredictions. We present a novel approach to address this problem by partially decoupling control from data flow: in order to perform the partitioning, we split the input in blocks of constant size (we propose 128 data elements); then, all elements in one block are compared with the pivot and the outcomes of the comparisons are stored in a buffer. In a second pass, the respective elements are rearranged. By doing so, we avoid conditional branches based on outcomes of comparisons at all (except for the final Insertionsort). Moreover, we prove that for a static branch predictor the average total number of branch mispredictions is at most epsilon n log n + O(n) for some small epsilon depending on the block size when sorting n elements. Our experimental results are promising: when sorting random integer data, we achieve an increase in speed (number of elements sorted per second) of more than 80% over the GCC implementation of C++ std::sort. Also for many other types of data and non-random inputs, there is still a significant speedup over std::sort. Only in few special cases like sorted or almost sorted inputs, std::sort can beat our implementation. Moreover, even on random input permutations, our implementation is even slightly faster than an implementation of the highly tuned Super Scalar Sample Sort, which uses a linear amount of additional space.

Cite as

Stefan Edelkamp and Armin Weiss. BlockQuicksort: Avoiding Branch Mispredictions in Quicksort. In 24th Annual European Symposium on Algorithms (ESA 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 57, pp. 38:1-38:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{edelkamp_et_al:LIPIcs.ESA.2016.38,
  author =	{Edelkamp, Stefan and Weiss, Armin},
  title =	{{BlockQuicksort: Avoiding Branch Mispredictions in Quicksort}},
  booktitle =	{24th Annual European Symposium on Algorithms (ESA 2016)},
  pages =	{38:1--38:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-015-6},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{57},
  editor =	{Sankowski, Piotr and Zaroliagis, Christos},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2016.38},
  URN =		{urn:nbn:de:0030-drops-63890},
  doi =		{10.4230/LIPIcs.ESA.2016.38},
  annote =	{Keywords: in-place sorting, Quicksort, branch mispredictions, lean programs}
}
Document
Automated Planning and Model Checking (Dagstuhl Seminar 14482)

Authors: Alessandro Cimatti, Stefan Edelkamp, Maria Fox, Daniele Magazzeni, and Erion Plaku

Published in: Dagstuhl Reports, Volume 4, Issue 11 (2015)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14482 "Automated Planning and Model Checking". There has been a lot of work on the exchanges between the areas of automated planning and model checking, based on the observation that a model-checking problem can be cast as a planning problem and vice-versa. The motivation for this seminar was to increase the synergy between the two research communities, and explore recent progress in the two areas in terms of techniques, tools and formalisms for describing planning and verification problems. The main outcomes were a greater common understanding of planning and model-checking issues and challenges, and greater appreciation of the crosswover between the modelling languages and methods. Different application domains were also explored, where planning and model-checking can be effectively integrated.

Cite as

Alessandro Cimatti, Stefan Edelkamp, Maria Fox, Daniele Magazzeni, and Erion Plaku. Automated Planning and Model Checking (Dagstuhl Seminar 14482). In Dagstuhl Reports, Volume 4, Issue 11, pp. 227-245, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@Article{cimatti_et_al:DagRep.4.11.227,
  author =	{Cimatti, Alessandro and Edelkamp, Stefan and Fox, Maria and Magazzeni, Daniele and Plaku, Erion},
  title =	{{Automated Planning and Model Checking (Dagstuhl Seminar 14482)}},
  pages =	{227--245},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{4},
  number =	{11},
  editor =	{Cimatti, Alessandro and Edelkamp, Stefan and Fox, Maria and Magazzeni, Daniele and Plaku, Erion},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.4.11.227},
  URN =		{urn:nbn:de:0030-drops-49731},
  doi =		{10.4230/DagRep.4.11.227},
  annote =	{Keywords: planning via model checking, directed model checking, plan validation, falsification, GPU-based state space exploration, hybrid systems, heuristic sea}
}
Document
09491 Abstracts Collection – Graph Search Engineering

Authors: Lubos Brim, Stefan Edelkamp, Eric A. Hansen, and Peter Sanders

Published in: Dagstuhl Seminar Proceedings, Volume 9491, Graph Search Engineering (2010)


Abstract
From the 29th November to the 4th December 2009, the Dagstuhl Seminar 09491 ``Graph Search Engineering '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Lubos Brim, Stefan Edelkamp, Eric A. Hansen, and Peter Sanders. 09491 Abstracts Collection – Graph Search Engineering. In Graph Search Engineering. Dagstuhl Seminar Proceedings, Volume 9491, pp. 1-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{brim_et_al:DagSemProc.09491.1,
  author =	{Brim, Lubos and Edelkamp, Stefan and Hansen, Eric A. and Sanders, Peter},
  title =	{{09491 Abstracts Collection – Graph Search Engineering}},
  booktitle =	{Graph Search Engineering},
  pages =	{1--31},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9491},
  editor =	{Lubos Brim and Stefan Edelkamp and Erik A. Hansen and Peter Sanders},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09491.1},
  URN =		{urn:nbn:de:0030-drops-24315},
  doi =		{10.4230/DagSemProc.09491.1},
  annote =	{Keywords: Model Checking, Artificial Intelligence, AI Planning, State Explosion Problem, Error Detection, Protocol Analysis, Software Verification and Validation, Heuristics, Pattern/Abstraction Databases, I/O Efficient Search, Solid State Disks, GPU}
}
Document
Dynamic State-Space Partitioning in External-Memory Graph Search

Authors: Rong Zhou and Eric A. Hansen

Published in: Dagstuhl Seminar Proceedings, Volume 9491, Graph Search Engineering (2010)


Abstract
State-of-the-art external-memory graph search algorithms rely on a hash function, or equivalently, a state-space projection function, that partitions the stored nodes of the state-space search graph into groups of nodes that are stored as separate files on disk. The scalability and efficiency of the search depends on properties of the partition: whether the number of unique nodes in a file always fits in RAM, the number of files into which the nodes of the state-space graph are partitioned, and how well the partitioning of the state space captures local structure in the graph. All previous work relies on a static partitioning of the state space. In this paper, we introduce a method for dynamic partitioning of the state-space search graph and show that it leads to substantial improvement of search performance.

Cite as

Rong Zhou and Eric A. Hansen. Dynamic State-Space Partitioning in External-Memory Graph Search. In Graph Search Engineering. Dagstuhl Seminar Proceedings, Volume 9491, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{zhou_et_al:DagSemProc.09491.2,
  author =	{Zhou, Rong and Hansen, Eric A.},
  title =	{{Dynamic State-Space Partitioning in External-Memory Graph Search}},
  booktitle =	{Graph Search Engineering},
  pages =	{1--7},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9491},
  editor =	{Lubos Brim and Stefan Edelkamp and Erik A. Hansen and Peter Sanders},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09491.2},
  URN =		{urn:nbn:de:0030-drops-24334},
  doi =		{10.4230/DagSemProc.09491.2},
  annote =	{Keywords: External-memory graph search, heuristic search}
}
Document
Landmarks, Critical Paths and Abstractions: What's the Difference Anyway?

Authors: Malte Helmert and Carmel Domshlak

Published in: Dagstuhl Seminar Proceedings, Volume 9491, Graph Search Engineering (2010)


Abstract
Current heuristic estimators for classical domain-independent planning are usually based on one of four ideas: delete relaxation, abstraction, critical paths, and, most recently, landmarks. Previously, these different ideas for deriving heuristic functions were largely unconnected. In my talk, I will show that these heuristics are in fact very closely related. Moreover, I will introduce a new admissible heuristic called the landmark cut heuristic which exploits this relationship. In our experiments, the landmark cut heuristic provides better estimates than other current admissible planning heuristics, especially on large problem instances.

Cite as

Malte Helmert and Carmel Domshlak. Landmarks, Critical Paths and Abstractions: What's the Difference Anyway?. In Graph Search Engineering. Dagstuhl Seminar Proceedings, Volume 9491, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{helmert_et_al:DagSemProc.09491.3,
  author =	{Helmert, Malte and Domshlak, Carmel},
  title =	{{Landmarks, Critical Paths and Abstractions: What's the Difference Anyway?}},
  booktitle =	{Graph Search Engineering},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9491},
  editor =	{Lubos Brim and Stefan Edelkamp and Erik A. Hansen and Peter Sanders},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09491.3},
  URN =		{urn:nbn:de:0030-drops-24324},
  doi =		{10.4230/DagSemProc.09491.3},
  annote =	{Keywords: Planning, heuristic search, heuristic functions}
}
Document
06172 Abstracts Collection – Directed Model Checking

Authors: Stefan Edelkamp, Stefan Leue, and Willem Visser

Published in: Dagstuhl Seminar Proceedings, Volume 6172, Directed Model Checking (2007)


Abstract
From 26.04.06 to 29.04.06, the Dagstuhl Seminar 06172 ``Directed Model Checking'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Stefan Edelkamp, Stefan Leue, and Willem Visser. 06172 Abstracts Collection – Directed Model Checking. In Directed Model Checking. Dagstuhl Seminar Proceedings, Volume 6172, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{edelkamp_et_al:DagSemProc.06172.1,
  author =	{Edelkamp, Stefan and Leue, Stefan and Visser, Willem},
  title =	{{06172 Abstracts Collection – Directed Model Checking}},
  booktitle =	{Directed Model Checking},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6172},
  editor =	{Stefan Edelkamp and Stefan Leue and Willem Visser},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06172.1},
  URN =		{urn:nbn:de:0030-drops-9469},
  doi =		{10.4230/DagSemProc.06172.1},
  annote =	{Keywords: Model Checking, Artificial Intelligence, AI Plannning, Guided Traversal, State Explosion Problem}
}
Document
06172 Executive Summary – Directed Model Checking

Authors: Stefan Edelkamp, Stefan Leue, and Willem Visser

Published in: Dagstuhl Seminar Proceedings, Volume 6172, Directed Model Checking (2007)


Abstract
This is a summary of the Dagstuhl Seminar 06172 {em Directed Model Checking} that was held 26 - 29 April 2006 at Schloss Dagstuhl, Germany. Directed Model Checking is a software and hardware verification technique that performs a systematic, heuristics guided search of the state space of the model to be analyzed. It hence reconciles classical model checking technology with intelligent, heuristics driven search that has a long tradition in artificial intelligence, in particular in the area of action planning. The benefits are short or even optimally short error trails, in some instances a more efficient exploration of the state space, and the applicability of state space search in some application areas in which unintelligent search would not yield useful results. The seminar brought together researchers from the system verification and the artificial intelligence domain in order to discuss the current state of the art, and to elicit and discuss research challenges and future directions.

Cite as

Stefan Edelkamp, Stefan Leue, and Willem Visser. 06172 Executive Summary – Directed Model Checking. In Directed Model Checking. Dagstuhl Seminar Proceedings, Volume 6172, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{edelkamp_et_al:DagSemProc.06172.2,
  author =	{Edelkamp, Stefan and Leue, Stefan and Visser, Willem},
  title =	{{06172 Executive Summary – Directed Model Checking}},
  booktitle =	{Directed Model Checking},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6172},
  editor =	{Stefan Edelkamp and Stefan Leue and Willem Visser},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06172.2},
  URN =		{urn:nbn:de:0030-drops-9443},
  doi =		{10.4230/DagSemProc.06172.2},
  annote =	{Keywords: Model checking, heuristics, state space search, software and hardware verification}
}
Document
Efficient Software Model Checking of Data Structure Properties

Authors: Chandrasekhar Boyapati and Paul Darga

Published in: Dagstuhl Seminar Proceedings, Volume 6172, Directed Model Checking (2007)


Abstract
This talk presents novel language and analysis techniques that significantly speed up software model checking of data structure properties. Consider checking a red-black tree implementation. Traditional software model checkers systematically generate all red-black tree states (within some given bounds) and check every red-black tree operation (such as insert, delete, or lookup) on every red-black tree state. Our key idea is as follows. As our checker checks a red-black tree operation $o$ on a red-black tree state $s$, it uses program analysis techniques to identify other red-black tree states $s'_1$, $s'_2$, ..., $s'_k$ on which the operation $o$ behaves similarly. Our analyses guarantee that if $o$ executes correctly on $s$, then $o$ will execute correctly on every $s'_i$. Our checker therefore does not need to check $o$ on any $s'_i$ once it checks $o$ on $s$. It thus safely prunes those state transitions from its search space, while still achieving complete test coverage within the bounded domain. Our preliminary results show {em orders of magnitude improvement} over previous approaches. We believe our techniques can make software model checking significantly faster, and thus enable checking of much larger programs and complex program properties than currently possible.

Cite as

Chandrasekhar Boyapati and Paul Darga. Efficient Software Model Checking of Data Structure Properties. In Directed Model Checking. Dagstuhl Seminar Proceedings, Volume 6172, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{boyapati_et_al:DagSemProc.06172.3,
  author =	{Boyapati, Chandrasekhar and Darga, Paul},
  title =	{{Efficient Software Model Checking of Data Structure Properties}},
  booktitle =	{Directed Model Checking},
  pages =	{1--19},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6172},
  editor =	{Stefan Edelkamp and Stefan Leue and Willem Visser},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06172.3},
  URN =		{urn:nbn:de:0030-drops-9450},
  doi =		{10.4230/DagSemProc.06172.3},
  annote =	{Keywords: Software Model Checking, Program Analysis, Linked Data Structures}
}
  • Refine by Author
  • 6 Edelkamp, Stefan
  • 2 Hansen, Eric A.
  • 2 Leue, Stefan
  • 2 Visser, Willem
  • 1 Boyapati, Chandrasekhar
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Design and analysis of algorithms

  • Refine by Keyword
  • 2 Artificial Intelligence
  • 2 Model Checking
  • 2 State Explosion Problem
  • 2 heuristic search
  • 1 AI Planning
  • Show More...

  • Refine by Type
  • 9 document

  • Refine by Publication Year
  • 3 2007
  • 3 2010
  • 1 2015
  • 1 2016
  • 1 2020

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail