28 Search Results for "Müller, Peter"

Volume

LIPIcs, Volume 74

31st European Conference on Object-Oriented Programming (ECOOP 2017)

ECOOP 2017, June 19-23, 2017, Barcelona, Spain

Editors: Peter Müller

Document
DOI: 10.4230/DagRep.13.7.66
Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281)

Authors: Arie Gurfinkel, Isabella Mastroeni, Antoine Miné, Peter Müller, and Anna Becchi

Published in: Dagstuhl Reports, Volume 13, Issue 7 (2024)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23281 "Theoretical Advances and Emerging Applications in Abstract Interpretation." Abstract Interpretation (AI) is a theory of the approximation of program semantics. Since its introduction in the 70s, it lead to insights into theoretical research in semantics, a rich and robust mathematical framework to discuss about semantic approximation and program analysis, and the design of effective program analysis tools that are now routinely used in this industry. The seminar brought together academic and industrial partners to assess the state of the art in AI as well as discuss its future. It considered its foundational aspects, connections with other formal methods, emergent applications, user needs in program verification, tool design and evaluation, as well as educational aspects and community management. Its goal was to collect new ideas and new perspectives on all these aspects of AI in order to pave the way for new applications.
Cite as

Arie Gurfinkel, Isabella Mastroeni, Antoine Miné, Peter Müller, and Anna Becchi. Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281). In Dagstuhl Reports, Volume 13, Issue 7, pp. 66-95, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{gurfinkel_et_al:DagRep.13.7.66,
  author =	{Gurfinkel, Arie and Mastroeni, Isabella and Min\'{e}, Antoine and M\"{u}ller, Peter and Becchi, Anna},
  title =	{{Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281)}},
  pages =	{66--95},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{7},
  editor =	{Gurfinkel, Arie and Mastroeni, Isabella and Min\'{e}, Antoine and M\"{u}ller, Peter and Becchi, Anna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.7.66},
  URN =		{urn:nbn:de:0030-drops-197759},
  doi =		{10.4230/DagRep.13.7.66},
  annote =	{Keywords: abstract domains, abstract interpretation, program semantics, program verification, static program analysis}
}
Document
DOI: 10.4230/OASIcs.EVCS.2023.18
On the Origins of Coccinelle

Authors: Julia Lawall

Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)

Abstract
Coccinelle is a program-transformation system for C code. It has been under development since 2005 and has been extensively used on the Linux kernel. The design of Coccinelle was inspired in part by the author’s previous experience in using Stratego/XT, developed by Eelco Visser. This paper reflects on some of Coccinelle’s design choices and their relation to Eelco Visser’s work.
Cite as

Julia Lawall. On the Origins of Coccinelle. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 18:1-18:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{lawall:OASIcs.EVCS.2023.18,
  author =	{Lawall, Julia},
  title =	{{On the Origins of Coccinelle}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{18:1--18:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.18},
  URN =		{urn:nbn:de:0030-drops-177884},
  doi =		{10.4230/OASIcs.EVCS.2023.18},
  annote =	{Keywords: Linux kernel, Coccinelle, Stratego/XT, program transformation}
}
Document
DOI: 10.4230/LIPIcs.TQC.2020.11
Fast and Effective Techniques for T-Count Reduction via Spider Nest Identities

Authors: Niel de Beaudrap, Xiaoning Bian, and Quanlong Wang

Published in: LIPIcs, Volume 158, 15th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2020)

Abstract
In fault-tolerant quantum computing systems, realising (approximately) universal quantum computation is usually described in terms of realising Clifford+T operations, which is to say a circuit of CNOT, Hadamard, and π/2-phase rotations, together with T operations (π/4-phase rotations). For many error correcting codes, fault-tolerant realisations of Clifford operations are significantly less resource-intensive than those of T gates, which motivates finding ways to realise the same transformation involving T-count (the number of T gates involved) which is as low as possible. Investigations into this problem [Matthew Amy et al., 2013; Gosset et al., 2014; Matthew Amy et al., 2014; Matthew Amy et al., 2018; Earl T. Campbell and Mark Howard, 2017; Matthew Amy and Michele Mosca, 2019] has led to observations that this problem is closely related to NP-hard tensor decomposition problems [Luke E. Heyfron and Earl T. Campbell, 2018] and is tantamount to the difficult problem of decoding exponentially long Reed-Muller codes [Matthew Amy and Michele Mosca, 2019]. This problem then presents itself as one for which must be content in practise with approximate optimisation, in which one develops an array of tactics to be deployed through some pragmatic strategy. In this vein, we describe techniques to reduce the T-count, based on the effective application of "spider nest identities": easily recognised products of parity-phase operations which are equivalent to the identity operation. We demonstrate the effectiveness of such techniques by obtaining improvements in the T-counts of a number of circuits, in run-times which are typically less than the time required to make a fresh cup of coffee.
Cite as

Niel de Beaudrap, Xiaoning Bian, and Quanlong Wang. Fast and Effective Techniques for T-Count Reduction via Spider Nest Identities. In 15th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 158, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{debeaudrap_et_al:LIPIcs.TQC.2020.11,
  author =	{de Beaudrap, Niel and Bian, Xiaoning and Wang, Quanlong},
  title =	{{Fast and Effective Techniques for T-Count Reduction via Spider Nest Identities}},
  booktitle =	{15th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2020)},
  pages =	{11:1--11:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-146-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{158},
  editor =	{Flammia, Steven T.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TQC.2020.11},
  URN =		{urn:nbn:de:0030-drops-120705},
  doi =		{10.4230/LIPIcs.TQC.2020.11},
  annote =	{Keywords: T-count, Parity-phase operations, Phase gadgets, Clifford hierarchy, ZX calculus}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.19
Counting of Teams in First-Order Team Logics

Authors: Anselm Haak, Juha Kontinen, Fabian Müller, Heribert Vollmer, and Fan Yang

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
We study descriptive complexity of counting complexity classes in the range from #P to #*NP. A corollary of Fagin’s characterization of NP by existential second-order logic is that #P can be logically described as the class of functions counting satisfying assignments to free relation variables in first-order formulae. In this paper we extend this study to classes beyond #P and extensions of first-order logic with team semantics. These team-based logics are closely related to existential second-order logic and its fragments, hence our results also shed light on the complexity of counting for extensions of first-order logic in Tarski’s semantics. Our results show that the class #*NP can be logically characterized by independence logic and existential second-order logic, whereas dependence logic and inclusion logic give rise to subclasses of #*NP and #P, respectively. We also study the function class generated by inclusion logic and relate it to the complexity class TotP, which is a subclass of #P. Our main technical result shows that the problem of counting satisfying assignments for monotone Boolean Sigma_1-formulae is #*NP-complete with respect to Turing reductions as well as complete for the function class generated by dependence logic with respect to first-order reductions.
Cite as

Anselm Haak, Juha Kontinen, Fabian Müller, Heribert Vollmer, and Fan Yang. Counting of Teams in First-Order Team Logics. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 19:1-19:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{haak_et_al:LIPIcs.MFCS.2019.19,
  author =	{Haak, Anselm and Kontinen, Juha and M\"{u}ller, Fabian and Vollmer, Heribert and Yang, Fan},
  title =	{{Counting of Teams in First-Order Team Logics}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{19:1--19:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.19},
  URN =		{urn:nbn:de:0030-drops-109634},
  doi =		{10.4230/LIPIcs.MFCS.2019.19},
  annote =	{Keywords: team-based logics, counting classes, finite model theory, descriptive complexity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.37
Resolution Lower Bounds for Refutation Statements

Authors: Michal Garlík

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
For any unsatisfiable CNF formula we give an exponential lower bound on the size of resolution refutations of a propositional statement that the formula has a resolution refutation. We describe three applications. (1) An open question in [Atserias and Müller, 2019] asks whether a certain natural propositional encoding of the above statement is hard for Resolution. We answer by giving an exponential size lower bound. (2) We show exponential resolution size lower bounds for reflection principles, thereby improving a result in [Albert Atserias and María Luisa Bonet, 2004]. (3) We provide new examples of CNFs that exponentially separate Res(2) from Resolution (an exponential separation of these two proof systems was originally proved in [Nathan Segerlind et al., 2004]).
Cite as

Michal Garlík. Resolution Lower Bounds for Refutation Statements. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 37:1-37:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{garlik:LIPIcs.MFCS.2019.37,
  author =	{Garl{\'\i}k, Michal},
  title =	{{Resolution Lower Bounds for Refutation Statements}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{37:1--37:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.37},
  URN =		{urn:nbn:de:0030-drops-109817},
  doi =		{10.4230/LIPIcs.MFCS.2019.37},
  annote =	{Keywords: reflection principles, refutation statements, Resolution, proof complexity}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.ECOOP.2017
LIPIcs, Volume 74, ECOOP'17, Complete Volume

Authors: Peter Müller

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
LIPIcs, Volume 74, ECOOP'17, Complete Volume
Cite as

31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Proceedings{muller:LIPIcs.ECOOP.2017,
  title =	{{LIPIcs, Volume 74, ECOOP'17, Complete Volume}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017},
  URN =		{urn:nbn:de:0030-drops-72993},
  doi =		{10.4230/LIPIcs.ECOOP.2017},
  annote =	{Keywords: Programming Techniques; Software Engineering}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ECOOP.2017.0
Front Matter, Table of Contents, Foreword, Conference Organization, External Reviewers, Authors

Authors: Peter Müller

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
Front Matter, Table of Contents, Foreword, Conference Organization, External Reviewers, Authors
Cite as

31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 0:i-0:xxvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{muller:LIPIcs.ECOOP.2017.0,
  author =	{M\"{u}ller, Peter},
  title =	{{Front Matter, Table of Contents, Foreword, Conference Organization, External Reviewers, Authors}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{0:i--0:xxvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.0},
  URN =		{urn:nbn:de:0030-drops-72783},
  doi =		{10.4230/LIPIcs.ECOOP.2017.0},
  annote =	{Keywords: Programming Techniques, Software Engineering}
}
Document
DOI: 10.4230/DagRep.6.5.56
Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201)

Authors: Julian Dolby, Orna Grumberg, Peter Müller, and Omer Tripp

Published in: Dagstuhl Reports, Volume 6, Issue 5 (2016)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 16201 "Synergies among Testing, Verification, and Repair for Concurrent Programs". This seminar builds upon, and is inspired by, several past seminars on program testing, verification, repair and combinations thereof. These include Dagstuhl Seminar 13021 "Symbolic Methods in Testing"; Dagstuhl Seminar 13061 "Fault Prediction, Localization and Repair"; Dagstuhl Seminar 14171 "Evaluating Software Verification Systems: Benchmarks and Competitions"; Dagstuhl Seminar 14352 "Next Generation Static Software Analysis Tools"; Dagstuhl Seminar 14442 "Symbolic Execution and Constraint Solving"; and Dagstuhl Seminar 15191 "Compositional Verification Methods for Next-Generation Concurrency". These were held in January 2013; February 2013; April 2014; August 2014; October 2014; and May 2015, respectively. Two notable contributions of Dagstuhl Seminar 16201, which distinguish it from these past seminars, are (i) the focus on concurrent programming, which introduces significant challenges to testing, verification and repair tools, as well as (ii) the goal of identifying and exploiting synergies between the testing, verification and repair research communities in light of common needs and goals.
Cite as

Julian Dolby, Orna Grumberg, Peter Müller, and Omer Tripp. Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201). In Dagstuhl Reports, Volume 6, Issue 5, pp. 56-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{dolby_et_al:DagRep.6.5.56,
  author =	{Dolby, Julian and Grumberg, Orna and M\"{u}ller, Peter and Tripp, Omer},
  title =	{{Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201)}},
  pages =	{56--71},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{6},
  number =	{5},
  editor =	{Dolby, Julian and Grumberg, Orna and M\"{u}ller, Peter and Tripp, Omer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.6.5.56},
  URN =		{urn:nbn:de:0030-drops-67203},
  doi =		{10.4230/DagRep.6.5.56},
  annote =	{Keywords: (automatic) bug repair, concurrency bugs, concurrent programming, deductive verification, interactive verification, linearizability, synchronization testing}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.639
Modular Verification of Finite Blocking in Non-terminating Programs

Authors: Pontus Boström and Peter Müller

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

Abstract
Most multi-threaded programs synchronize threads via blocking operations such as acquiring locks or joining other threads. An important correctness property of such programs is for each thread to make progress, that is, not to be blocked forever. For programs in which all threads terminate, progress essentially follows from deadlock freedom. However, for the common case that a program contains non-terminating threads such as servers or actors, deadlock freedom is not sufficient. For instance, a thread may be blocked forever by a non-terminating thread if it attempts to join that thread or to acquire a lock held by that thread. In this paper, we present a verification technique for finite blocking in non-terminating programs. The key idea is to track explicitly whether a thread has an obligation to perform an operation that unblocks another thread, for instance, an obligation to release a lock or to terminate. Each obligation is associated with a measure to ensure that it is fulfilled within finitely many steps. Obligations may be used in specifications, which makes verification modular. We formalize our technique via an encoding into Boogie, which treats different kinds of obligations uniformly. It subsumes termination checking as a special case.
Cite as

Pontus Boström and Peter Müller. Modular Verification of Finite Blocking in Non-terminating Programs. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 639-663, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bostrom_et_al:LIPIcs.ECOOP.2015.639,
  author =	{Bostr\"{o}m, Pontus and M\"{u}ller, Peter},
  title =	{{Modular Verification of Finite Blocking in Non-terminating Programs}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{639--663},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.639},
  URN =		{urn:nbn:de:0030-drops-52416},
  doi =		{10.4230/LIPIcs.ECOOP.2015.639},
  annote =	{Keywords: Program verification, concurrency, liveness, progress, obligations}
}
Document
DOI: 10.4230/DFU.Vol3.11041.157
Audio Content-Based Music Retrieval

Authors: Peter Grosche, Meinard Müller, and Joan Serrà

Published in: Dagstuhl Follow-Ups, Volume 3, Multimodal Music Processing (2012)

Abstract
The rapidly growing corpus of digital audio material requires novel retrieval strategies for exploring large music collections. Traditional retrieval strategies rely on metadata that describe the actual audio content in words. In the case that such textual descriptions are not available, one requires content-based retrieval strategies which only utilize the raw audio material. In this contribution, we discuss content-based retrieval strategies that follow the query-by-example paradigm: given an audio query, the task is to retrieve all documents that are somehow similar or related to the query from a music collection. Such strategies can be loosely classified according to their "specificity", which refers to the degree of similarity between the query and the database documents. Here, high specificity refers to a strict notion of similarity, whereas low specificity to a rather vague one. Furthermore, we introduce a second classification principle based on "granularity", where one distinguishes between fragment-level and document-level retrieval. Using a classification scheme based on specificity and granularity, we identify various classes of retrieval scenarios, which comprise "audio identification", "audio matching", and "version identification". For these three important classes, we give an overview of representative state-of-the-art approaches, which also illustrate the sometimes subtle but crucial differences between the retrieval scenarios. Finally, we give an outlook on a user-oriented retrieval system, which combines the various retrieval strategies in a unified framework.
Cite as

Peter Grosche, Meinard Müller, and Joan Serrà. Audio Content-Based Music Retrieval. In Multimodal Music Processing. Dagstuhl Follow-Ups, Volume 3, pp. 157-174, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InCollection{grosche_et_al:DFU.Vol3.11041.157,
  author =	{Grosche, Peter and M\"{u}ller, Meinard and Serr\`{a}, Joan},
  title =	{{Audio Content-Based Music Retrieval}},
  booktitle =	{Multimodal Music Processing},
  pages =	{157--174},
  series =	{Dagstuhl Follow-Ups},
  ISBN =	{978-3-939897-37-8},
  ISSN =	{1868-8977},
  year =	{2012},
  volume =	{3},
  editor =	{M\"{u}ller, Meinard and Goto, Masataka and Schedl, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DFU.Vol3.11041.157},
  URN =		{urn:nbn:de:0030-drops-34711},
  doi =		{10.4230/DFU.Vol3.11041.157},
  annote =	{Keywords: music retrieval, content-based, query-by-example, audio identification, audio matching, cover song identification}
}
Document
DOI: 10.4230/DagSemProc.10281.6
Compiling Geometric Algebra Computations into Reconfigurable Hardware Accelerators

Authors: Jens Huthmann, Peter Müller, Florian Stock, Dietmar Hildenbrand, and Andreas Koch

Published in: Dagstuhl Seminar Proceedings, Volume 10281, Dynamically Reconfigurable Architectures (2010)

Abstract
Geometric Algebra (GA), a generalization of quaternions and complex numbers, is a very powerful framework for intuitively expressing and manipulating the complex geometric relationships common to engineering problems. However, actual processing of GA expressions is very compute intensive, and acceleration is generally required for practical use. GPUs and FPGAs offer such acceleration, while requiring only low-power per operation. In this paper, we present key components of a proof-of-concept compile flow combining symbolic and hardware optimization techniques to automatically generate hardware accelerators from the abstract GA descriptions that are suitable for high-performance embedded computing.
Cite as

Jens Huthmann, Peter Müller, Florian Stock, Dietmar Hildenbrand, and Andreas Koch. Compiling Geometric Algebra Computations into Reconfigurable Hardware Accelerators. In Dynamically Reconfigurable Architectures. Dagstuhl Seminar Proceedings, Volume 10281, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{huthmann_et_al:DagSemProc.10281.6,
  author =	{Huthmann, Jens and M\"{u}ller, Peter and Stock, Florian and Hildenbrand, Dietmar and Koch, Andreas},
  title =	{{Compiling Geometric Algebra Computations into Reconfigurable  Hardware Accelerators}},
  booktitle =	{Dynamically Reconfigurable Architectures},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10281},
  editor =	{Peter M. Athanas and J\"{u}rgen Becker and J\"{u}rgen Teich and Ingrid Verbauwhede},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10281.6},
  URN =		{urn:nbn:de:0030-drops-28389},
  doi =		{10.4230/DagSemProc.10281.6},
  annote =	{Keywords: Geometric Algebra FPGA High-Level-Compiler Gaalop}
}
Document
DOI: 10.4230/DagSemProc.09051.7
Towards Automated Processing of Folk Song Recordings

Authors: Meinard Müller, Peter Grosche, and Frans Wiering

Published in: Dagstuhl Seminar Proceedings, Volume 9051, Knowledge representation for intelligent music processing (2009)

Abstract
Folk music is closely related to the musical culture of a specific nation or region. Even though folk songs have been passed down mainly by oral tradition, most musicologists study the relation between folk songs on the basis of symbolic music descriptions, which are obtained by transcribing recorded tunes into a score-like representation. Due to the complexity of audio recordings, once having the transcriptions, the original recorded tunes are often no longer used in the actual folk song research even though they still may contain valuable information. In this paper, we present various techniques for making audio recordings more easily accessible for music researchers. In particular, we show how one can use synchronization techniques to automatically segment and annotate the recorded songs. The processed audio recordings can then be made accessible along with a symbolic transcript by means of suitable visualization, searching, and navigation interfaces to assist folk song researchers to conduct large scale investigations comprising the audio material.
Cite as

Meinard Müller, Peter Grosche, and Frans Wiering. Towards Automated Processing of Folk Song Recordings. In Knowledge representation for intelligent music processing. Dagstuhl Seminar Proceedings, Volume 9051, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{muller_et_al:DagSemProc.09051.7,
  author =	{M\"{u}ller, Meinard and Grosche, Peter and Wiering, Frans},
  title =	{{Towards Automated Processing of Folk Song Recordings}},
  booktitle =	{Knowledge representation for intelligent music processing},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9051},
  editor =	{Eleanor Selfridge-Field and Frans Wiering and Geraint A. Wiggins},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09051.7},
  URN =		{urn:nbn:de:0030-drops-19666},
  doi =		{10.4230/DagSemProc.09051.7},
  annote =	{Keywords: Folk songs, audio, segmentation, music synchronization, annotation, performance analysis}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2008.1584
Efficient On-Trip Timetable Information in the Presence of Delays

Authors: Lennart Frede, Matthias Müller-Hannemann, and Mathias Schnee

Published in: OASIcs, Volume 9, 8th Workshop on Algorithmic Approaches for Transportation Modeling, Optimization, and Systems (ATMOS'08) (2008)

Abstract
The search for train connections in state-of-the-art commercial timetable information systems is based on a static schedule. Unfortunately, public transportation systems suffer from delays for various reasons. Thus, dynamic changes of the planned schedule have to be taken into account. A system that has access to delay information of trains (and uses this information within search queries) can provide valid alternatives in case a train change breaks. Additionally, it can be used to actively guide passengers as these alternatives may be presented before the passenger is already stranded at a station due to a broken transfer. In this work we present an approach which takes a stream of delay information and schedule changes on short notice (partial train cancellations, extra trains) into account. Primary delays of trains may cause a cascade of so-called secondary delays of other trains which have to wait according to certain waiting policies between connecting trains. We introduce the concept of a dependency graph to efficiently calculate and update all primary and secondary delays. This delay information is then incorporated into a time-expanded search graph which has to be updated dynamically. These update operations are quite complex, but turn out to be not time-critical in a fully realistic scenario. We finally present a case study with data provided by Deutsche Bahn AG showing that this approach has been successfully integrated into our multi-criteria timetable information system MOTIS and can handle massive delay data streams instantly.
Cite as

Lennart Frede, Matthias Müller-Hannemann, and Mathias Schnee. Efficient On-Trip Timetable Information in the Presence of Delays. In 8th Workshop on Algorithmic Approaches for Transportation Modeling, Optimization, and Systems (ATMOS'08). Open Access Series in Informatics (OASIcs), Volume 9, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{frede_et_al:OASIcs.ATMOS.2008.1584,
  author =	{Frede, Lennart and M\"{u}ller-Hannemann, Matthias and Schnee, Mathias},
  title =	{{Efficient On-Trip Timetable Information in the Presence of Delays}},
  booktitle =	{8th Workshop on Algorithmic Approaches for Transportation Modeling, Optimization, and Systems (ATMOS'08)},
  pages =	{1--16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-07-1},
  ISSN =	{2190-6807},
  year =	{2008},
  volume =	{9},
  editor =	{Fischetti, Matteo and Widmayer, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2008.1584},
  URN =		{urn:nbn:de:0030-drops-15843},
  doi =		{10.4230/OASIcs.ATMOS.2008.1584},
  annote =	{Keywords: Timetable information system, primary and secondary delays dependency graph, dynamic graph update}
}
Document
DOI: 10.4230/DagSemProc.07171.1
07171 Abstracts Collection – Visual Computing – Convergence of Computer Graphics and Computer Vision

Authors: Markus Gross, Heinrich Müller, Hans-Peter Seidel, and Harry Shum

Published in: Dagstuhl Seminar Proceedings, Volume 7171, Visual Computing - Convergence of Computer Graphics and Computer Vision (2008)

Abstract
From 22.04. to 27.04.2007, the Dagstuhl Seminar 07171 ``Visual Computing - Convergence of Computer Graphics and Computer Vision'' 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

Markus Gross, Heinrich Müller, Hans-Peter Seidel, and Harry Shum. 07171 Abstracts Collection – Visual Computing – Convergence of Computer Graphics and Computer Vision. In Visual Computing - Convergence of Computer Graphics and Computer Vision. Dagstuhl Seminar Proceedings, Volume 7171, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{gross_et_al:DagSemProc.07171.1,
  author =	{Gross, Markus and M\"{u}ller, Heinrich and Seidel, Hans-Peter and Shum, Harry},
  title =	{{07171 Abstracts Collection – Visual Computing – Convergence of Computer Graphics and Computer Vision}},
  booktitle =	{Visual Computing - Convergence of Computer Graphics and Computer Vision},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7171},
  editor =	{Markus Gross and Heinrich M\"{u}ller and Hans-Peter Seidel and Harry Shum},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07171.1},
  URN =		{urn:nbn:de:0030-drops-15044},
  doi =		{10.4230/DagSemProc.07171.1},
  annote =	{Keywords: Image- and video-based modeling and rendering, perception-guided modeling and rendering, texture synthesis, scattering and reflectance measurement rendering, capturing reality (appearance, motion) from images, 3D acquisition and display, 3D reconstruction, image and model compression, computation}
}
  • Refine by Author
  • 8 Müller, Peter
  • 5 Müller, Heinrich
  • 5 Seidel, Hans-Peter
  • 4 Gross, Markus
  • 4 Müller, Rudolf
  • Show More...

  • Refine by Classification
  • 1 Computer systems organization → Quantum computing
  • 1 Software and its engineering
  • 1 Software and its engineering → Automated static analysis
  • 1 Software and its engineering → Completeness
  • 1 Software and its engineering → Correctness
  • Show More...

  • Refine by Keyword
  • 3 Mechanism Design
  • 2 3D acquisition and display
  • 2 3D reconstruction
  • 2 Behavioral Economics
  • 2 Combinatorial Auctions
  • Show More...

  • Refine by Type
  • 27 document
  • 1 volume

  • Refine by Publication Year
  • 6 2007
  • 3 2008
  • 3 2017
  • 2 2006
  • 2 2019
  • 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