19 Search Results for "Becker, Christoph"

Document
DOI: 10.4230/LIPIcs.AFT.2024.24
Investigating Wrench Attacks: Physical Attacks Targeting Cryptocurrency Users

Authors: Marilyne Ordekian, Gilberto Atondo-Siu, Alice Hutchings, and Marie Vasek

Published in: LIPIcs, Volume 316, 6th Conference on Advances in Financial Technologies (AFT 2024)

Abstract
Cryptocurrency wrench attacks are physical attacks targeting cryptocurrency users in the real world to illegally obtain cryptocurrencies. These attacks significantly undermine the efficacy of existing digital security norms when confronted with real-world threats. We present the first comprehensive study on wrench attacks. We propose a theoretical approach to defining wrench attacks per criminal law norms, and an interdisciplinary empirical approach to measure their incidence. Leveraging three data sources, we perform crime script analysis, detecting incidents globally across 10 interviews with victims and experts, 146 news articles, and 37 online forums. Our findings reveal diverse groups of attackers ranging from organized crime groups to friends and family, various modi operandi, and different forms of attacks varying from blackmail to murder. Despite existing since Bitcoin’s early days, these attacks are underreported due to revictimization fears. Additionally, unlike other cryptocurrency crimes, users with advanced security experience were not immune to them. We identify potential vulnerabilities in users' behavior and encourage cryptocurrency holders to lean into digital as well as physical safety measures to protect themselves and their cryptocurrency. We offer actionable recommendations for the security community and regulators, highlighting the double-edged sword of Know Your Customer policies.
Cite as

Marilyne Ordekian, Gilberto Atondo-Siu, Alice Hutchings, and Marie Vasek. Investigating Wrench Attacks: Physical Attacks Targeting Cryptocurrency Users. In 6th Conference on Advances in Financial Technologies (AFT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 316, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ordekian_et_al:LIPIcs.AFT.2024.24,
  author =	{Ordekian, Marilyne and Atondo-Siu, Gilberto and Hutchings, Alice and Vasek, Marie},
  title =	{{Investigating Wrench Attacks: Physical Attacks Targeting Cryptocurrency Users}},
  booktitle =	{6th Conference on Advances in Financial Technologies (AFT 2024)},
  pages =	{24:1--24:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-345-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{316},
  editor =	{B\"{o}hme, Rainer and Kiffer, Lucianna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2024.24},
  URN =		{urn:nbn:de:0030-drops-209609},
  doi =		{10.4230/LIPIcs.AFT.2024.24},
  annote =	{Keywords: cryptocurrency, Bitcoin, crime, wrench attack, physical attack}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.SAT.2024.1
Models and Counter-Models of Quantified Boolean Formulas (Invited Talk)

Authors: Martina Seidl

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

Abstract
Because of the duality of universal and existential quantification, quantified Boolean formulas (QBF), the extension of propositional logic with quantifiers over the Boolean variables, have not only solutions in terms of models for true formulas like in SAT. Also false QBFs have solutions in terms of counter-models. Both models and counter-models can be represented as certain binary trees or as sets of Boolean functions reflecting the dependencies among the variables of a formula. Such solutions encode the answers to application problems for which QBF solvers are employed like the plan for a planning problem or the error trace of a verification problem. Therefore, models and counter-models are at the core of theory and practice of QBF solving. In this invited talk, we survey approaches that deal with models and counter-models of QBFs and identify some open challenges.
Cite as

Martina Seidl. Models and Counter-Models of Quantified Boolean Formulas (Invited Talk). In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 1:1-1:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{seidl:LIPIcs.SAT.2024.1,
  author =	{Seidl, Martina},
  title =	{{Models and Counter-Models of Quantified Boolean Formulas}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{1:1--1:7},
  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.1},
  URN =		{urn:nbn:de:0030-drops-205238},
  doi =		{10.4230/LIPIcs.SAT.2024.1},
  annote =	{Keywords: Quantified Boolean Formula, Solution Extraction, Solution Counting}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.13
Entailing Generalization Boosts Enumeration

Authors: Dror Fried, Alexander Nadel, Roberto Sebastiani, and Yogev Shalmon

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

Abstract
Given a combinational circuit Γ with a single output o, AllSAT-CT is the problem of enumerating all solutions of Γ. Recently, we introduced several state-of-the-art AllSAT-CT algorithms based on satisfying generalization, which generalizes a given total Boolean solution to a smaller ternary solution that still satisfies the circuit. We implemented them in our open-source tool HALL. In this work we draw upon recent theoretical works suggesting that utilizing generalization algorithms, which can produce solutions that entail the circuit without satisfying it, may enhance enumeration. After considering the theory and adapting it to our needs, we enrich HALL’s AllSAT-CT algorithms by incorporating several newly implemented generalization schemes and additional SAT solvers. By conducting extensive experiments we show that entailing generalization substantially boosts HALL’s performance and quality (where quality corresponds to the number of reported generalized solutions per instance), with the best results achieved by combining satisfying and entailing generalization.
Cite as

Dror Fried, Alexander Nadel, Roberto Sebastiani, and Yogev Shalmon. Entailing Generalization Boosts Enumeration. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{fried_et_al:LIPIcs.SAT.2024.13,
  author =	{Fried, Dror and Nadel, Alexander and Sebastiani, Roberto and Shalmon, Yogev},
  title =	{{Entailing Generalization Boosts Enumeration}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{13:1--13:14},
  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.13},
  URN =		{urn:nbn:de:0030-drops-205351},
  doi =		{10.4230/LIPIcs.SAT.2024.13},
  annote =	{Keywords: Generalization, Minimization, Prime Implicant, AllSAT, SAT, Circuits}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.21
Dynamic Blocked Clause Elimination for Projected Model Counting

Authors: Jean-Marie Lagniez, Pierre Marquis, and Armin Biere

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

Abstract
In this paper, we explore the application of blocked clause elimination for projected model counting. This is the problem of determining the number of models ‖∃ X . Σ‖ of a propositional formula Σ after eliminating a given set X of variables existentially. Although blocked clause elimination is a well-known technique for SAT solving, its direct application to model counting is challenging as in general it changes the number of models. However, we demonstrate, by focusing on projected variables during the blocked clause search, that blocked clause elimination can be leveraged while preserving the correct model count. To take advantage of blocked clause elimination in an efficient way during model counting, a novel data structure and associated algorithms are introduced. Our proposed approach is implemented in the model counter d4. Our experiments demonstrate the computational benefits of our new method of blocked clause elimination for projected model counting.
Cite as

Jean-Marie Lagniez, Pierre Marquis, and Armin Biere. Dynamic Blocked Clause Elimination for Projected Model Counting. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{lagniez_et_al:LIPIcs.SAT.2024.21,
  author =	{Lagniez, Jean-Marie and Marquis, Pierre and Biere, Armin},
  title =	{{Dynamic Blocked Clause Elimination for Projected Model Counting}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{21:1--21:17},
  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.21},
  URN =		{urn:nbn:de:0030-drops-205430},
  doi =		{10.4230/LIPIcs.SAT.2024.21},
  annote =	{Keywords: Projected model counting, blocked clause elimination, propositional logic}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2024.6
Optimizing Per-Core Priorities to Minimize End-To-End Latencies

Authors: Francesco Paladino, Alessandro Biondi, Enrico Bini, and Paolo Pazzaglia

Published in: LIPIcs, Volume 298, 36th Euromicro Conference on Real-Time Systems (ECRTS 2024)

Abstract
Logical Execution Time (LET) allows decoupling the schedule of real-time periodic tasks from their communication, with the advantage of isolating the communication pattern from the variability of the schedule. However, when such tasks are organized in chains, the usage of LET at the task level does not necessarily transfer the same LET properties to the chain level. In this paper, we extend a LET-like model from tasks to chains spanning over multiple cores. We leverage the designed constant latency chains to optimize per-core priority assignment. Finally, we also provide a set of heuristic algorithms, that are compared in a large-scale experimental evaluation.
Cite as

Francesco Paladino, Alessandro Biondi, Enrico Bini, and Paolo Pazzaglia. Optimizing Per-Core Priorities to Minimize End-To-End Latencies. In 36th Euromicro Conference on Real-Time Systems (ECRTS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 298, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{paladino_et_al:LIPIcs.ECRTS.2024.6,
  author =	{Paladino, Francesco and Biondi, Alessandro and Bini, Enrico and Pazzaglia, Paolo},
  title =	{{Optimizing Per-Core Priorities to Minimize End-To-End Latencies}},
  booktitle =	{36th Euromicro Conference on Real-Time Systems (ECRTS 2024)},
  pages =	{6:1--6:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-324-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{298},
  editor =	{Pellizzoni, Rodolfo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2024.6},
  URN =		{urn:nbn:de:0030-drops-203094},
  doi =		{10.4230/LIPIcs.ECRTS.2024.6},
  annote =	{Keywords: Cause-Effect Chains, Logical Execution Time, End-to-End Latency, Design Optimization, Task Priorities, Data Age, Reaction Time}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2020.50
Low Diameter Graph Decompositions by Approximate Distance Computation

Authors: Ruben Becker, Yuval Emek, and Christoph Lenzen

Published in: LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020)

Abstract
In many models for large-scale computation, decomposition of the problem is key to efficient algorithms. For distance-related graph problems, it is often crucial that such a decomposition results in clusters of small diameter, while the probability that an edge is cut by the decomposition scales linearly with the length of the edge. There is a large body of literature on low diameter graph decomposition with small edge cutting probabilities, with all existing techniques heavily building on single source shortest paths (SSSP) computations. Unfortunately, in many theoretical models for large-scale computations, the SSSP task constitutes a complexity bottleneck. Therefore, it is desirable to replace exact SSSP computations with approximate ones. However this imposes a fundamental challenge since the existing constructions of low diameter graph decomposition with small edge cutting probabilities inherently rely on the subtractive form of the triangle inequality, which fails to hold under distance approximation. The current paper overcomes this obstacle by developing a technique termed blurry ball growing. By combining this technique with a clever algorithmic idea of Miller et al. (SPAA 2013), we obtain a construction of low diameter decompositions with small edge cutting probabilities which replaces exact SSSP computations by (a small number of) approximate ones. The utility of our approach is showcased by deriving efficient algorithms that work in the CONGEST, PRAM, and semi-streaming models of computation. As an application, we obtain metric tree embedding algorithms in the vein of Bartal (FOCS 1996) whose computational complexities in these models are optimal up to polylogarithmic factors. Our embeddings have the additional useful property that the tree can be mapped back to the original graph such that each edge is "used" only logaritmically many times, which is of interest for capacitated problems and simulating CONGEST algorithms on the tree into which the graph is embedded.
Cite as

Ruben Becker, Yuval Emek, and Christoph Lenzen. Low Diameter Graph Decompositions by Approximate Distance Computation. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 50:1-50:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:LIPIcs.ITCS.2020.50,
  author =	{Becker, Ruben and Emek, Yuval and Lenzen, Christoph},
  title =	{{Low Diameter Graph Decompositions by Approximate Distance Computation}},
  booktitle =	{11th Innovations in Theoretical Computer Science Conference (ITCS 2020)},
  pages =	{50:1--50:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-134-4},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{151},
  editor =	{Vidick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.50},
  URN =		{urn:nbn:de:0030-drops-117355},
  doi =		{10.4230/LIPIcs.ITCS.2020.50},
  annote =	{Keywords: graph decompositions, metric tree embeddings, distributed graph algorithms, parallel graph algorithms, (semi-)streaming graph algorithms}
}
Document
DOI: 10.4230/DagRep.9.7.40
Values in Computing (Dagstuhl Seminar 19291)

Authors: Christoph Becker, Gregor Engels, Andrew Feenberg, Maria Angela Ferrario, and Geraldine Fitzpatrick

Published in: Dagstuhl Reports, Volume 9, Issue 7 (2020)

Abstract
Values are deeply held principles guiding decisions of individuals, groups and organizations. Computing technologies are inevitably affected by values: through their design, values become embodied and enacted. However, some values are easier to quantify and articulate than others; for example, the financial value of a software product is easier to measure than its `fairness'. As a result, less measurable values are often dismissed in decision making processes as lacking evidence. This is particularly problematic since research shows that less measurable values tend to be more strongly associated with sustainable practices than easier to quantify ones; it also indicates that the systems we design are likely to be inadequate for tackling long-term complex societal problems such as environmental change and health-related challenges that so often computing technologies are asked to address. This seminar aims to examine the complex relations between values, computing technologies and society. It does so by bringing together practitioners and researchers from several areas within and beyond computer science, including human computer interaction, software engineering, computer ethics, moral philosophy, philosophy of technology, data science and critical data studies. The outcomes include concrete cases examined through diverse disciplinary perspectives and guidelines for values in computing research, development and education, which are expressed in this report.
Cite as

Christoph Becker, Gregor Engels, Andrew Feenberg, Maria Angela Ferrario, and Geraldine Fitzpatrick. Values in Computing (Dagstuhl Seminar 19291). In Dagstuhl Reports, Volume 9, Issue 7, pp. 40-77, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{becker_et_al:DagRep.9.7.40,
  author =	{Becker, Christoph and Engels, Gregor and Feenberg, Andrew and Ferrario, Maria Angela and Fitzpatrick, Geraldine},
  title =	{{Values in Computing (Dagstuhl Seminar 19291)}},
  pages =	{40--77},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{9},
  number =	{7},
  editor =	{Becker, Christoph and Engels, Gregor and Feenberg, Andrew and Ferrario, Maria Angela and Fitzpatrick, Geraldine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.9.7.40},
  URN =		{urn:nbn:de:0030-drops-116358},
  doi =		{10.4230/DagRep.9.7.40},
  annote =	{Keywords: computing in society, responsible innovation, sustainability informatics computer ethics, philosophy of technology and moral philosophy}
}
Document
DOI: 10.4230/LIPIcs.DISC.2019.4
Distributed Algorithms for Low Stretch Spanning Trees

Authors: Ruben Becker, Yuval Emek, Mohsen Ghaffari, and Christoph Lenzen

Published in: LIPIcs, Volume 146, 33rd International Symposium on Distributed Computing (DISC 2019)

Abstract
Given an undirected graph with integer edge lengths, we study the problem of approximating the distances in the graph by a spanning tree based on the notion of stretch. Our main contribution is a distributed algorithm in the CONGEST model of computation that constructs a random spanning tree with the guarantee that the expected stretch of every edge is O(log^{3} n), where n is the number of nodes in the graph. If the graph is unweighted, then this algorithm can be implemented to run in O(D) rounds, where D is the hop-diameter of the graph, thus being asymptotically optimal. In the weighted case, the run-time of our algorithm matches the currently best known bound for exact distance computations, i.e., O~ (min{sqrt{n D}, sqrt{n} D^{1 / 4} + n^{3 / 5} + D}). We stress that this is the first distributed construction of spanning trees leading to poly-logarithmic expected stretch with non-trivial running time.
Cite as

Ruben Becker, Yuval Emek, Mohsen Ghaffari, and Christoph Lenzen. Distributed Algorithms for Low Stretch Spanning Trees. In 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 4:1-4:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:LIPIcs.DISC.2019.4,
  author =	{Becker, Ruben and Emek, Yuval and Ghaffari, Mohsen and Lenzen, Christoph},
  title =	{{Distributed Algorithms for Low Stretch Spanning Trees}},
  booktitle =	{33rd International Symposium on Distributed Computing (DISC 2019)},
  pages =	{4:1--4:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-126-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{146},
  editor =	{Suomela, Jukka},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2019.4},
  URN =		{urn:nbn:de:0030-drops-113116},
  doi =		{10.4230/LIPIcs.DISC.2019.4},
  annote =	{Keywords: distributed graph algorithms, low-stretch spanning trees, CONGEST model, ball decomposition, star decomposition}
}
Document
DOI: 10.4230/LIPIcs.DISC.2017.7
Near-Optimal Approximate Shortest Paths and Transshipment in Distributed and Streaming Models

Authors: Ruben Becker, Andreas Karrenbauer, Sebastian Krinninger, and Christoph Lenzen

Published in: LIPIcs, Volume 91, 31st International Symposium on Distributed Computing (DISC 2017)

Abstract
We present a method for solving the shortest transshipment problem - also known as uncapacitated minimum cost flow - up to a multiplicative error of (1 + epsilon) in undirected graphs with non-negative integer edge weights using a tailored gradient descent algorithm. Our gradient descent algorithm takes epsilon^(-3) polylog(n) iterations, and in each iteration it needs to solve an instance of the transshipment problem up to a multiplicative error of polylog(n), where n is the number of nodes. In particular, this allows us to perform a single iteration by computing a solution on a sparse spanner of logarithmic stretch. Using a careful white-box analysis, we can further extend the method to finding approximate solutions for the single-source shortest paths (SSSP) problem. As a consequence, we improve prior work by obtaining the following results: (1) Broadcast CONGEST model: (1 + epsilon)-approximate SSSP using ~O((sqrt(n) + D) epsilon^(-O(1))) rounds, where D is the (hop) diameter of the network. (2) Broadcast congested clique model: (1 + epsilon)-approximate shortest transshipment and SSSP using ~O(epsilon^(-O(1))) rounds. (3) Multipass streaming model: (1 + epsilon)-approximate shortest transshipment and SSSP using ~O(n) space and ~O(epsilon^(-O(1))) passes. The previously fastest SSSP algorithms for these models leverage sparse hop sets. We bypass the hop set construction; computing a spanner is sufficient with our method. The above bounds assume non-negative integer edge weights that are polynomially bounded in n; for general non-negative weights, running times scale with the logarithm of the maximum ratio between non-zero weights. In case of asymmetric costs for traversing an edge in opposite directions, running times scale with the maximum ratio between the costs of both directions over all edges.
Cite as

Ruben Becker, Andreas Karrenbauer, Sebastian Krinninger, and Christoph Lenzen. Near-Optimal Approximate Shortest Paths and Transshipment in Distributed and Streaming Models. In 31st International Symposium on Distributed Computing (DISC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 91, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:LIPIcs.DISC.2017.7,
  author =	{Becker, Ruben and Karrenbauer, Andreas and Krinninger, Sebastian and Lenzen, Christoph},
  title =	{{Near-Optimal Approximate Shortest Paths and Transshipment in Distributed and Streaming Models}},
  booktitle =	{31st International Symposium on Distributed Computing (DISC 2017)},
  pages =	{7:1--7:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-053-8},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{91},
  editor =	{Richa, Andr\'{e}a},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2017.7},
  URN =		{urn:nbn:de:0030-drops-80031},
  doi =		{10.4230/LIPIcs.DISC.2017.7},
  annote =	{Keywords: Shortest Paths, Shortest Transshipment, Undirected Min-cost Flow, Gradient Descent, Spanner}
}
Document
DOI: 10.4230/DagMan.6.1.1
Engineering Academic Software (Dagstuhl Perspectives Workshop 16252)

Authors: Alice Allen, Cecilia Aragon, Christoph Becker, Jeffrey Carver, Andrei Chis, Benoit Combemale, Mike Croucher, Kevin Crowston, Daniel Garijo, Ashish Gehani, Carole Goble, Robert Haines, Robert Hirschfeld, James Howison, Kathryn Huff, Caroline Jay, Daniel S. Katz, Claude Kirchner, Katie Kuksenok, Ralf Lämmel, Oscar Nierstrasz, Matt Turk, Rob van Nieuwpoort, Matthew Vaughn, and Jurgen J. Vinju

Published in: Dagstuhl Manifestos, Volume 6, Issue 1 (2017)

Abstract
Software is often a critical component of scientific research. It can be a component of the academic research methods used to produce research results, or it may itself be an academic research result. Software, however, has rarely been considered to be a citable artifact in its own right. With the advent of open-source software, artifact evaluation committees of conferences, and journals that include source code and running systems as part of the published artifacts, we foresee that software will increasingly be recognized as part of the academic process. The quality and sustainability of this software must be accounted for, both a prioro and a posteriori. The Dagstuhl Perspectives Workshop on "Engineering Academic Software" has examined the strengths, weaknesses, risks, and opportunities of academic software engineering. A key outcome of the workshop is this Dagstuhl Manifesto, serving as a roadmap towards future professional software engineering for software-based research instruments and other software produced and used in an academic context. The manifesto is expressed in terms of a series of actionable "pledges" that users and developers of academic research software can take as concrete steps towards improving the environment in which that software is produced.
Cite as

Alice Allen, Cecilia Aragon, Christoph Becker, Jeffrey Carver, Andrei Chis, Benoit Combemale, Mike Croucher, Kevin Crowston, Daniel Garijo, Ashish Gehani, Carole Goble, Robert Haines, Robert Hirschfeld, James Howison, Kathryn Huff, Caroline Jay, Daniel S. Katz, Claude Kirchner, Katie Kuksenok, Ralf Lämmel, Oscar Nierstrasz, Matt Turk, Rob van Nieuwpoort, Matthew Vaughn, and Jurgen J. Vinju. Engineering Academic Software (Dagstuhl Perspectives Workshop 16252). In Dagstuhl Manifestos, Volume 6, Issue 1, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{allen_et_al:DagMan.6.1.1,
  author =	{Allen, Alice and Aragon, Cecilia and Becker, Christoph and Carver, Jeffrey and Chis, Andrei and Combemale, Benoit and Croucher, Mike and Crowston, Kevin and Garijo, Daniel and Gehani, Ashish and Goble, Carole and Haines, Robert and Hirschfeld, Robert and Howison, James and Huff, Kathryn and Jay, Caroline and Katz, Daniel S. and Kirchner, Claude and Kuksenok, Katie and L\"{a}mmel, Ralf and Nierstrasz, Oscar and Turk, Matt and van Nieuwpoort, Rob and Vaughn, Matthew and Vinju, Jurgen J.},
  title =	{{Engineering Academic Software (Dagstuhl Perspectives Workshop 16252)}},
  pages =	{1--20},
  journal =	{Dagstuhl Manifestos},
  ISSN =	{2193-2433},
  year =	{2017},
  volume =	{6},
  number =	{1},
  editor =	{Allen, Alice and Aragon, Cecilia and Becker, Christoph and Carver, Jeffrey and Chis, Andrei and Combemale, Benoit and Croucher, Mike and Crowston, Kevin and Garijo, Daniel and Gehani, Ashish and Goble, Carole and Haines, Robert and Hirschfeld, Robert and Howison, James and Huff, Kathryn and Jay, Caroline and Katz, Daniel S. and Kirchner, Claude and Kuksenok, Katie and L\"{a}mmel, Ralf and Nierstrasz, Oscar and Turk, Matt and van Nieuwpoort, Rob and Vaughn, Matthew and Vinju, Jurgen J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagMan.6.1.1},
  URN =		{urn:nbn:de:0030-drops-71468},
  doi =		{10.4230/DagMan.6.1.1},
  annote =	{Keywords: Academic software, Research software, Software citation, Software sustainability}
}
Document
DOI: 10.4230/DagSemProc.10291.5
Challenges in preservation (planning)

Authors: Christoph Becker

Published in: Dagstuhl Seminar Proceedings, Volume 10291, Automation in Digital Preservation (2010)

Abstract
This short paper attempts to highlight some challenges to be tackled by DP research in the next years, taking as a starting point the perspective of preservation planning. These challenges are in short: (1) Scalability (up and down) requiring (2) measurement of relevant decision factors, in turn requiring (3) benchmarking and ground truth. (4) Quality-aware emulation. (5) Move from the current closed-systems approach to open structures that accomodate evolving knowledge. (6) Move from post-obsolescence actions to 'longevity engineering'.
Cite as

Christoph Becker. Challenges in preservation (planning). In Automation in Digital Preservation. Dagstuhl Seminar Proceedings, Volume 10291, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{becker:DagSemProc.10291.5,
  author =	{Becker, Christoph},
  title =	{{Challenges in preservation (planning)}},
  booktitle =	{Automation in Digital Preservation},
  pages =	{1--5},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10291},
  editor =	{Jean-Pierre Chanod and Milena Dobreva and Andreas Rauber and Seamus Ross},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10291.5},
  URN =		{urn:nbn:de:0030-drops-27689},
  doi =		{10.4230/DagSemProc.10291.5},
  annote =	{Keywords: Preservation planning, software engineering, scalability, measurements, benchmarking, ground truth, longevity}
}
Document
DOI: 10.4230/DagSemProc.10271.4
Towards more Dependable Verification of Mixed-Signal Systems

Authors: Florian Schupfer and Christoph Grimm

Published in: Dagstuhl Seminar Proceedings, Volume 10271, Verification over discrete-continuous boundaries (2010)

Abstract
The verification of complex mixed-signal systems is a challenge, especially considering the impact of parameter variations. Besides the established approaches like Monte-Carlo or Corner-Case simulation, a novel semi-symbolic approach emerged in recent years. In this approach, parameter variations and tolerances are maintained as symbolic ranges during numerical simulation runs by using affine arithmetic. Maintaining parameter variations and tolerances in a symbolic way significantly increases verification coverage. In the following we give a brief introduction and an overview of research on semi-symbolic simulation of both circuits and systems and discuss possible application for system level verification and optimization.
Cite as

Florian Schupfer and Christoph Grimm. Towards more Dependable Verification of Mixed-Signal Systems. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{schupfer_et_al:DagSemProc.10271.4,
  author =	{Schupfer, Florian and Grimm, Christoph},
  title =	{{Towards more Dependable Verification of Mixed-Signal Systems}},
  booktitle =	{Verification over discrete-continuous boundaries},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10271},
  editor =	{Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.4},
  URN =		{urn:nbn:de:0030-drops-27911},
  doi =		{10.4230/DagSemProc.10271.4},
  annote =	{Keywords: Affine Arithmetic, Range based methods, Verification, Semi-symbolic simulation}
}
Document
DOI: 10.4230/DagSemProc.09461.5
SWORD – Module-based SAT Solving

Authors: Robert Wille, Jean Christoph Jung, Andre Sülflow, and Rolf Drechsler

Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)

Abstract
In the paper, SWORD is described – a decision procedure for bit-vector logic that uses SAT techniques and exploits word level information. The main idea of SWORD is based on the following observation: While current SAT solvers perform very well on instances with a large number of logic operations, their performance on arithmetic operations degrades with increasing data-path width. In contrast, pure word-level approaches are able to handle arithmetic operations very fast, but suffer from irregularities in the word-level structure (e.g. bit slicing). SWORD tries to combine the best of both worlds: On the one hand, it includes fast propagation, sophisticated data structures, as well as advanced techniques like non-chronological backtracking and learning from modern SAT solvers. On the other hand word-level information is exploited in the decision heuristic and during propagation.
Cite as

Robert Wille, Jean Christoph Jung, Andre Sülflow, and Rolf Drechsler. SWORD – Module-based SAT Solving. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{wille_et_al:DagSemProc.09461.5,
  author =	{Wille, Robert and Jung, Jean Christoph and S\"{u}lflow, Andre and Drechsler, Rolf},
  title =	{{SWORD – Module-based SAT Solving}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9461},
  editor =	{Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.5},
  URN =		{urn:nbn:de:0030-drops-25069},
  doi =		{10.4230/DagSemProc.09461.5},
  annote =	{Keywords: SAT Solver, Word Level, SAT Modulo Theories}
}
Document
DOI: 10.4230/DagSemRep.297
Computer Aided Design and Test - BDDs versus SAT (Dagstuhl Seminar 01051)

Authors: Bernd Becker, Masahiro Fujita, Christoph Meinel, and Fabio Somenzi

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Bernd Becker, Masahiro Fujita, Christoph Meinel, and Fabio Somenzi. Computer Aided Design and Test - BDDs versus SAT (Dagstuhl Seminar 01051). Dagstuhl Seminar Report 297, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2001)

Copy BibTex To Clipboard

@TechReport{becker_et_al:DagSemRep.297,
  author =	{Becker, Bernd and Fujita, Masahiro and Meinel, Christoph and Somenzi, Fabio},
  title =	{{Computer Aided Design and Test - BDDs versus SAT (Dagstuhl Seminar 01051)}},
  pages =	{1--25},
  ISSN =	{1619-0203},
  year =	{2001},
  type = 	{Dagstuhl Seminar Report},
  number =	{297},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.297},
  URN =		{urn:nbn:de:0030-drops-151811},
  doi =		{10.4230/DagSemRep.297},
}
Document
DOI: 10.4230/DagSemRep.229
Computer Aided Design and Test Decision Diagrams - Concepts and Applications (Dagstuhl Seminar 99041)

Authors: Bernd Becker, Christoph Meinel, Shin-Ichi Minato, and Fabio Somenzi

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Bernd Becker, Christoph Meinel, Shin-Ichi Minato, and Fabio Somenzi. Computer Aided Design and Test Decision Diagrams - Concepts and Applications (Dagstuhl Seminar 99041). Dagstuhl Seminar Report 229, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1999)

Copy BibTex To Clipboard

@TechReport{becker_et_al:DagSemRep.229,
  author =	{Becker, Bernd and Meinel, Christoph and Minato, Shin-Ichi and Somenzi, Fabio},
  title =	{{Computer Aided Design and Test Decision Diagrams - Concepts and Applications (Dagstuhl Seminar 99041)}},
  pages =	{1--16},
  ISSN =	{1619-0203},
  year =	{1999},
  type = 	{Dagstuhl Seminar Report},
  number =	{229},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.229},
  URN =		{urn:nbn:de:0030-drops-151155},
  doi =		{10.4230/DagSemRep.229},
}
  • Refine by Author
  • 6 Becker, Bernd
  • 6 Meinel, Christoph
  • 3 Becker, Christoph
  • 3 Becker, Ruben
  • 3 Lenzen, Christoph
  • Show More...

  • Refine by Classification
  • 2 Mathematics of computing → Graph algorithms
  • 2 Theory of computation → Automated reasoning
  • 2 Theory of computation → Distributed algorithms
  • 1 Applied computing → Digital cash
  • 1 Applied computing → Law
  • Show More...

  • Refine by Keyword
  • 2 distributed graph algorithms
  • 1 (semi-)streaming graph algorithms
  • 1 Academic software
  • 1 Affine Arithmetic
  • 1 AllSAT
  • Show More...

  • Refine by Type
  • 19 document

  • Refine by Publication Year
  • 5 2024
  • 3 2010
  • 2 2017
  • 2 2019
  • 1 1991
  • Show More...

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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact