Search Results

Documents authored by van de Pol, Jaco

Document
Complete Volume
DOI: 10.4230/LIPIcs.CONCUR.2025
LIPIcs, Volume 348, CONCUR 2025, Complete Volume

Authors: Patricia Bouyer and Jaco van de Pol

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
LIPIcs, Volume 348, CONCUR 2025, Complete Volume
Cite as

36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 1-774, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Proceedings{bouyer_et_al:LIPIcs.CONCUR.2025,
  title =	{{LIPIcs, Volume 348, CONCUR 2025, Complete Volume}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{1--774},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025},
  URN =		{urn:nbn:de:0030-drops-244431},
  doi =		{10.4230/LIPIcs.CONCUR.2025},
  annote =	{Keywords: LIPIcs, Volume 348, CONCUR 2025, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CONCUR.2025.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Patricia Bouyer and Jaco van de Pol

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2025.0,
  author =	{Bouyer, Patricia and van de Pol, Jaco},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{0:i--0:xii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.0},
  URN =		{urn:nbn:de:0030-drops-244386},
  doi =		{10.4230/LIPIcs.CONCUR.2025.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.16
Depth-Optimal Quantum Layout Synthesis as SAT

Authors: Anna B. Jakobsen, Anders B. Clausen, Jaco van de Pol, and Irfansha Shaik

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Quantum circuits consist of gates applied to qubits. Current quantum hardware platforms impose connectivity restrictions on binary CX gates. Hence, Layout Synthesis is an important step to transpile quantum circuits before they can be executed. Since CX gates are noisy, it is important to reduce the CX count or CX depth of the mapped circuits. We provide a new and efficient encoding of Quantum-circuit Layout Synthesis in SAT. Previous SAT encodings focused on gate count and CX-gate count. Our encoding instead guarantees that we find mapped circuits with minimal circuit depth or minimal CX-gate depth. We use incremental SAT solving and parallel plans for an efficient encoding. This results in speedups of more than 10-100x compared to OLSQ2, which guarantees depth-optimality. But minimizing depth still takes more time than minimizing gate count with Q-Synth. We correlate the noise reduction achieved by simulating circuits after (CX)-count and (CX)-depth reduction. We find that minimizing for CX-count correlates better with reducing noise than minimizing for CX-depth. However, taking into account both CX-count and CX-depth provides the best noise reduction.
Cite as

Anna B. Jakobsen, Anders B. Clausen, Jaco van de Pol, and Irfansha Shaik. Depth-Optimal Quantum Layout Synthesis as SAT. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jakobsen_et_al:LIPIcs.SAT.2025.16,
  author =	{Jakobsen, Anna B. and Clausen, Anders B. and van de Pol, Jaco and Shaik, Irfansha},
  title =	{{Depth-Optimal Quantum Layout Synthesis as SAT}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{16:1--16:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.16},
  URN =		{urn:nbn:de:0030-drops-237501},
  doi =		{10.4230/LIPIcs.SAT.2025.16},
  annote =	{Keywords: Quantum Layout Synthesis, Transpiling, Circuit Mapping, Incremental SAT, Parallel Plans}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.28
CNOT-Optimal Clifford Synthesis as SAT

Authors: Irfansha Shaik and Jaco van de Pol

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Clifford circuit optimization is an important step in the quantum compilation pipeline. Major compilers employ heuristic approaches. While they are fast, their results are often suboptimal. Minimization of noisy gates, like 2-qubit CNOT gates, is crucial for practical computing. Exact approaches have been proposed to fill the gap left by heuristic approaches. Among these are SAT based approaches that optimize gate count or depth, but they suffer from scalability issues. Further, they do not guarantee optimality on more important metrics like CNOT count or CNOT depth. A recent work proposed an exhaustive search only on Clifford circuits in a certain normal form to guarantee CNOT count optimality. But an exhaustive approach cannot scale beyond 6 qubits. In this paper, we incorporate search restricted to Clifford normal forms in a SAT encoding to guarantee CNOT count optimality. By allowing parallel plans, we propose a second SAT encoding that optimizes CNOT depth. By taking advantage of flexibility in SAT based approaches, we also handle connectivity restrictions in hardware platforms, and allow for qubit relabeling. We have implemented the above encodings and variations in our open source tool Q-Synth. In experiments, our encodings significantly outperform existing SAT approaches on random Clifford circuits. We consider practical VQE and Feynman benchmarks to compare with TKET and Qiskit compilers. In all-to-all connectivity, we observe reductions up to 32.1% in CNOT count and 48.1% in CNOT depth. Overall, we observe better results than TKET in the CNOT count and depth. We also experiment with connectivity restrictions of major quantum platforms. Compared to Qiskit, we observe up to 30.3% CNOT count and 35.9% CNOT depth further reduction.
Cite as

Irfansha Shaik and Jaco van de Pol. CNOT-Optimal Clifford Synthesis as SAT. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{shaik_et_al:LIPIcs.SAT.2025.28,
  author =	{Shaik, Irfansha and van de Pol, Jaco},
  title =	{{CNOT-Optimal Clifford Synthesis as SAT}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{28:1--28:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.28},
  URN =		{urn:nbn:de:0030-drops-237621},
  doi =		{10.4230/LIPIcs.SAT.2025.28},
  annote =	{Keywords: Circuit Synthesis, Circuit Optimization, Quantum Circuits, Propositional Satisfiability, Parallel Plans, Clifford Circuits, Encodings}
}
Artifact
Software
DOI: 10.4230/artifacts.22468
Q-Synth

Authors: Irfansha Shaik and Jaco van de Pol

Abstract
Cite as

Irfansha Shaik, Jaco van de Pol. Q-Synth (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22468,
   title = {{Q-Synth}}, 
   author = {Shaik, Irfansha and van de Pol, Jaco},
   note = {Software, version 2.0., IFD (Innovation Fund Denmark), swhId: \href{https://archive.softwareheritage.org/swh:1:dir:be31c57364bd541c6b65afac80603e9004cf4008;origin=https://github.com/irfansha/Q-Synth;visit=swh:1:snp:f376849e93533f1d9039b7cd543ed56b6edcf01d;anchor=swh:1:rev:553d54c9942b73a0246328d42565caaaaac38117}{\texttt{swh:1:dir:be31c57364bd541c6b65afac80603e9004cf4008}} (visited on 2024-11-28)},
   url = {https://github.com/irfansha/Q-Synth},
   doi = {10.4230/artifacts.22468},
}
Artifact
Software
DOI: 10.4230/artifacts.22469
Q-Synth v2.0 release

Authors: Irfansha Shaik and Jaco van de Pol

Abstract
Cite as

Irfansha Shaik, Jaco van de Pol. Q-Synth v2.0 release (Software, Github Tag). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22469,
   title = {{Q-Synth v2.0 release}}, 
   author = {Shaik, Irfansha and van de Pol, Jaco},
   note = {Software, version 2.0., IFD (Innovation Fund Denmark), swhId: \href{https://archive.softwareheritage.org/swh:1:dir:be31c57364bd541c6b65afac80603e9004cf4008;origin=https://github.com/irfansha/Q-Synth;visit=swh:1:snp:f376849e93533f1d9039b7cd543ed56b6edcf01d;anchor=swh:1:rev:553d54c9942b73a0246328d42565caaaaac38117}{\texttt{swh:1:dir:be31c57364bd541c6b65afac80603e9004cf4008}} (visited on 2024-11-28)},
   url = {https://github.com/irfansha/Q-Synth/releases/tag/Q-Synth-v2.0-SAT2024},
   doi = {10.4230/artifacts.22469},
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.26
Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits

Authors: Irfansha Shaik and Jaco van de Pol

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Layout synthesis is mapping a quantum circuit to a quantum processor. SWAP gate insertions are needed for scheduling 2-qubit gates only on connected physical qubits. With the ever-increasing number of qubits in NISQ processors, scalable layout synthesis is of utmost importance. With large optimality gaps observed in heuristic approaches, scalable exact methods are needed. While recent exact and near-optimal approaches scale to moderate circuits, large deep circuits are still out of scope. In this work, we propose a SAT encoding based on parallel plans that apply 1 SWAP and a group of CNOTs at each time step. Using domain-specific information, we maintain optimality in parallel plans while scaling to large and deep circuits. From our results, we show the scalability of our approach which significantly outperforms leading exact and near-optimal approaches (up to 100x). For the first time, we can optimally map several 8, 14, and 16 qubit circuits onto 54, 80, and 127 qubit platforms with up to 17 SWAPs. While adding optimal SWAPs, we also report near-optimal depth in our mapped circuits.
Cite as

Irfansha Shaik and Jaco van de Pol. Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{shaik_et_al:LIPIcs.SAT.2024.26,
  author =	{Shaik, Irfansha and van de Pol, Jaco},
  title =	{{Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.26},
  URN =		{urn:nbn:de:0030-drops-205487},
  doi =		{10.4230/LIPIcs.SAT.2024.26},
  annote =	{Keywords: Layout Synthesis, Transpiling, Qubit Mapping and Routing, Quantum Circuits, Propositional Satisfiability, Parallel Plans}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.24
Validation of QBF Encodings with Winning Strategies

Authors: Irfansha Shaik, Maximilian Heisinger, Martina Seidl, and Jaco van de Pol

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
When using a QBF solver for solving application problems encoded to quantified Boolean formulas (QBFs), mainly two things can potentially go wrong: (1) the solver could be buggy and return a wrong result or (2) the encoding could be incorrect. To ensure the correctness of solvers, sophisticated fuzzing and testing techniques have been presented. To ultimately trust a solving result, solvers have to provide a proof certificate that can be independently checked. Much less attention, however, has been paid to the question how to ensure the correctness of encodings. The validation of QBF encodings is particularly challenging because of the variable dependencies introduced by the quantifiers. In contrast to SAT, the solution of a true QBF is not simply a variable assignment, but a winning strategy. For each existential variable x, a winning strategy provides a function that defines how to set x based on the values of the universal variables that precede x in the quantifier prefix. Winning strategies for false formulas are defined dually. In this paper, we provide a tool for validating encodings using winning strategies and interactive game play with a QBF solver. As the representation of winning strategies can get huge, we also introduce validation based on partial winning strategies. Finally, we employ winning strategies for testing if two different encodings of one problem have the same solutions.
Cite as

Irfansha Shaik, Maximilian Heisinger, Martina Seidl, and Jaco van de Pol. Validation of QBF Encodings with Winning Strategies. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 24:1-24:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{shaik_et_al:LIPIcs.SAT.2023.24,
  author =	{Shaik, Irfansha and Heisinger, Maximilian and Seidl, Martina and van de Pol, Jaco},
  title =	{{Validation of QBF Encodings with Winning Strategies}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{24:1--24:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.24},
  URN =		{urn:nbn:de:0030-drops-184863},
  doi =		{10.4230/LIPIcs.SAT.2023.24},
  annote =	{Keywords: QBF, Validation, Winning Strategy, Equivalence, Certificates}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2023.18
Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism

Authors: Magnus Madsen and Jaco van de Pol

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

Abstract
We present purity reflection, a programming language feature that enables higher-order functions to inspect the purity of their function arguments and to vary their behavior based on this information. The upshot is that operations on data structures can selectively use lazy and/or parallel evaluation while ensuring that side effects are never lost or re-ordered. The technique builds on a recent Hindley-Milner style type and effect system based on Boolean unification which supports both effect polymorphism and complete type inference. We illustrate that avoiding the so-called 'poisoning problem' is crucial to support purity reflection. We propose several new data structures that use purity reflection to switch between eager and lazy, sequential and parallel evaluation. We propose a DelayList, which is maximally lazy but switches to eager evaluation for impure operations. We also propose a DelayMap which is maximally lazy in its values, but also exploits eager and parallel evaluation. We implement purity reflection as an extension of the Flix programming language. We present a new effect-aware form of monomorphization that eliminates purity reflection at compile-time. And finally, we evaluate the cost of this new monomorphization on compilation time and on code size, and determine that it is minimal.
Cite as

Magnus Madsen and Jaco van de Pol. Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 18:1-18:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{madsen_et_al:LIPIcs.ECOOP.2023.18,
  author =	{Madsen, Magnus and van de Pol, Jaco},
  title =	{{Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{18:1--18:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.18},
  URN =		{urn:nbn:de:0030-drops-182112},
  doi =		{10.4230/LIPIcs.ECOOP.2023.18},
  annote =	{Keywords: type and effect systems, purity reflection, lazy evaluation, parallel evaluation}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2019.4
Concurrent Algorithms and Data Structures for Model Checking (Invited Talk)

Authors: Jaco van de Pol

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
Model checking is a successful method for checking properties on the state space of concurrent, reactive systems. Since it is based on exhaustive search, scaling this method to industrial systems has been a challenge since its conception. Research has focused on clever data structures and algorithms, to reduce the size of the state space or its representation; smart search heuristics, to reveal potential bugs and counterexamples early; and high-performance computing, to deploy the brute force processing power of clusters of compute-servers. The main challenge is to combine these approaches - brute-force alone (when implemented carefully) can bring a linear speedup in the number of processors. This is great, since it reduces model-checking times from days to minutes. On the other hand, proper algorithms and data structures can lead to exponential gains. Therefore, the parallelization bonus is only real if we manage to speedup clever algorithms. There are some obstacles though: many linear-time graph algorithms depend on a depth-first exploration order, which is hard to parallelize. Examples include the detection of strongly connected components (SCC) and the nested depth-first-search (NDFS) algorithm. Both are used in model checking LTL properties. Symbolic representations, like binary decision diagrams (BDDs), reduce model checking to "pointer-chasing", leading to irregular memory-access patterns. This poses severe challenges on achieving actual speedup in (clusters of) modern multi-core computer architectures. This talk presents some of the solutions found over the last 10 years, which led to the high-performance model checker LTSmin [Gijs Kant et al., 2015]. These include parallel NDFS (based on the PhD thesis of Alfons Laarman [Alfons Laarman, 2014]), the parallel detection of SCCs with concurrent Union-Find (based on the PhD thesis of Vincent Bloemen [Vincent Bloemen, 2019]), and concurrent BDDs (based on the PhD thesis of Tom van Dijk [Tom van Dijk, 2016]). Finally, I will sketch a perspective on moving forward from high-performance model checking to high-performance synthesis algorithms. Examples include parameter synthesis for stochastic and timed systems, and strategy synthesis for (stochastic and timed) games.
Cite as

Jaco van de Pol. Concurrent Algorithms and Data Structures for Model Checking (Invited Talk). In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, p. 4:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{vandepol:LIPIcs.CONCUR.2019.4,
  author =	{van de Pol, Jaco},
  title =	{{Concurrent Algorithms and Data Structures for Model Checking}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{4:1--4:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.4},
  URN =		{urn:nbn:de:0030-drops-109066},
  doi =		{10.4230/LIPIcs.CONCUR.2019.4},
  annote =	{Keywords: model checking, parallel algorithms, concurrent datastructures}
}
Document
DOI: 10.4230/DagSemProc.08332.3
A Typical Verification Challenge for the GRID

Authors: Jaco van de Pol

Published in: Dagstuhl Seminar Proceedings, Volume 8332, Distributed Verification and Grid Computing (2008)

Abstract
A typical verification challenge for the GRID community is presented. The concrete challenge is to implement a simple recursive algorithm for finding the strongly connected components in a graph. The graph is typically stored in the collective memory of a number of computers, so a distributed algorithm is necessary. The implementation should be efficient and scalable, and separate synchronization and implementation details from the purely algorithmic aspects. In the end, a framework is envisaged for distributed algorithms on very large graphs. This would be useful to explore various alternative algorithmic choices.
Cite as

Jaco van de Pol. A Typical Verification Challenge for the GRID. In Distributed Verification and Grid Computing. Dagstuhl Seminar Proceedings, Volume 8332, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{vandepol:DagSemProc.08332.3,
  author =	{van de Pol, Jaco},
  title =	{{A Typical Verification Challenge for the GRID}},
  booktitle =	{Distributed Verification and Grid Computing},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8332},
  editor =	{Henri E. Bal and Lubos Brim and Martin Leucker},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08332.3},
  URN =		{urn:nbn:de:0030-drops-16293},
  doi =		{10.4230/DagSemProc.08332.3},
  annote =	{Keywords: Strongly connected components, distributed algorithms, breadth first search}
}
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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact