10 Search Results for "Müller-Hermes, Alexander"


Document
Deep Learning and Knowledge Integration for Music Audio Analysis (Dagstuhl Seminar 22082)

Authors: Meinard Müller, Rachel Bittner, Juhan Nam, Michael Krause, and Yigitcan Özer

Published in: Dagstuhl Reports, Volume 12, Issue 2 (2022)


Abstract
Given the increasing amount of digital music, the development of computational tools that allow users to find, organize, analyze, and interact with music has become central to the research field known as Music Information Retrieval (MIR). As in general multimedia processing, many of the recent advances in MIR have been driven by techniques based on deep learning (DL). There is a growing trend to relax problem-specific modeling constraints from MIR systems and instead apply relatively generic DL-based approaches that rely on large quantities of data. In the Dagstuhl Seminar 22082, we critically examined this trend, discussing the strengths and weaknesses of these approaches using music as a challenging application domain. We mainly focused on music analysis tasks applied to audio representations (rather than symbolic music representations) to give the seminar cohesion. In this context, we systematically explored how musical knowledge can be integrated into or relaxed from computational pipelines. We then discussed how this choice could affect the explainability of models or the vulnerability to data biases and confounding factors. Furthermore, besides explainability and generalization, we also addressed efficiency, ethical and educational aspects considering traditional model-based and recent data-driven methods. In this report, we give an overview of the various contributions and results of the seminar. We start with an executive summary describing the main topics, goals, and group activities. Then, we give an overview of the participants' stimulus talks and subsequent discussions (listed alphabetically by the main contributor’s last name) and summarize further activities, including group discussions and music sessions.

Cite as

Meinard Müller, Rachel Bittner, Juhan Nam, Michael Krause, and Yigitcan Özer. Deep Learning and Knowledge Integration for Music Audio Analysis (Dagstuhl Seminar 22082). In Dagstuhl Reports, Volume 12, Issue 2, pp. 103-133, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@Article{muller_et_al:DagRep.12.2.103,
  author =	{M\"{u}ller, Meinard and Bittner, Rachel and Nam, Juhan and Krause, Michael and \"{O}zer, Yigitcan},
  title =	{{Deep Learning and Knowledge Integration for Music Audio Analysis (Dagstuhl Seminar 22082)}},
  pages =	{103--133},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{12},
  number =	{2},
  editor =	{M\"{u}ller, Meinard and Bittner, Rachel and Nam, Juhan and Krause, Michael and \"{O}zer, Yigitcan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.12.2.103},
  URN =		{urn:nbn:de:0030-drops-169333},
  doi =		{10.4230/DagRep.12.2.103},
  annote =	{Keywords: Audio signal processing, deep learning, knowledge representation, music information retrieval, user interaction and interfaces}
}
Document
A Lower Bound on the Space Overhead of Fault-Tolerant Quantum Computation

Authors: Omar Fawzi, Alexander Müller-Hermes, and Ala Shayeghi

Published in: LIPIcs, Volume 215, 13th Innovations in Theoretical Computer Science Conference (ITCS 2022)


Abstract
The threshold theorem is a fundamental result in the theory of fault-tolerant quantum computation stating that arbitrarily long quantum computations can be performed with a polylogarithmic overhead provided the noise level is below a constant level. A recent work by Fawzi, Grospellier and Leverrier (FOCS 2018) building on a result by Gottesman (QIC 2013) has shown that the space overhead can be asymptotically reduced to a constant independent of the circuit provided we only consider circuits with a length bounded by a polynomial in the width. In this work, using a minimal model for quantum fault tolerance, we establish a general lower bound on the space overhead required to achieve fault tolerance. For any non-unitary qubit channel 𝒩 and any quantum fault tolerance schemes against i.i.d. noise modeled by 𝒩, we prove a lower bound of max{Q(𝒩)^{-1}n,α_𝒩 log T} on the number of physical qubits, for circuits of length T and width n. Here, Q(𝒩) denotes the quantum capacity of 𝒩 and α_𝒩 > 0 is a constant only depending on the channel 𝒩. In our model, we allow for qubits to be replaced by fresh ones during the execution of the circuit and in the case of unital noise, we allow classical computation to be free and perfect. This improves upon results that assumed classical computations to be also affected by noise, and that sometimes did not allow for fresh qubits to be added. Along the way, we prove an exponential upper bound on the maximal length of fault-tolerant quantum computation with amplitude damping noise resolving a conjecture by Ben-Or, Gottesman and Hassidim (2013).

Cite as

Omar Fawzi, Alexander Müller-Hermes, and Ala Shayeghi. A Lower Bound on the Space Overhead of Fault-Tolerant Quantum Computation. In 13th Innovations in Theoretical Computer Science Conference (ITCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 215, pp. 68:1-68:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{fawzi_et_al:LIPIcs.ITCS.2022.68,
  author =	{Fawzi, Omar and M\"{u}ller-Hermes, Alexander and Shayeghi, Ala},
  title =	{{A Lower Bound on the Space Overhead of Fault-Tolerant Quantum Computation}},
  booktitle =	{13th Innovations in Theoretical Computer Science Conference (ITCS 2022)},
  pages =	{68:1--68:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-217-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{215},
  editor =	{Braverman, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2022.68},
  URN =		{urn:nbn:de:0030-drops-156649},
  doi =		{10.4230/LIPIcs.ITCS.2022.68},
  annote =	{Keywords: Fault-tolerant quantum computation, quantum error correction}
}
Document
Towards Improved Robustness of Public Transport by a Machine-Learned Oracle

Authors: Matthias Müller-Hannemann, Ralf Rückert, Alexander Schiewe, and Anita Schöbel

Published in: OASIcs, Volume 96, 21st Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2021)


Abstract
The design and optimization of public transport systems is a highly complex and challenging process. Here, we focus on the trade-off between two criteria which shall make the transport system attractive for passengers: their travel time and the robustness of the system. The latter is time-consuming to evaluate. A passenger-based evaluation of robustness requires a performance simulation with respect to a large number of possible delay scenarios, making this step computationally very expensive. For optimizing the robustness, we hence apply a machine-learned oracle from previous work which approximates the robustness of a public transport system. We apply this oracle to bi-criteria optimization of integrated public transport planning (timetabling and vehicle scheduling) in two ways: First, we explore a local search based framework studying several variants of neighborhoods. Second, we evaluate a genetic algorithm. Computational experiments with artificial and close to real-word benchmark datasets yield promising results. In all cases, an existing pool of solutions (i.e., public transport plans) can be significantly improved by finding a number of new non-dominated solutions, providing better and different trade-offs between robustness and travel time.

Cite as

Matthias Müller-Hannemann, Ralf Rückert, Alexander Schiewe, and Anita Schöbel. Towards Improved Robustness of Public Transport by a Machine-Learned Oracle. In 21st Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2021). Open Access Series in Informatics (OASIcs), Volume 96, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{mullerhannemann_et_al:OASIcs.ATMOS.2021.3,
  author =	{M\"{u}ller-Hannemann, Matthias and R\"{u}ckert, Ralf and Schiewe, Alexander and Sch\"{o}bel, Anita},
  title =	{{Towards Improved Robustness of Public Transport by a Machine-Learned Oracle}},
  booktitle =	{21st Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2021)},
  pages =	{3:1--3:20},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-213-6},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{96},
  editor =	{M\"{u}ller-Hannemann, Matthias and Perea, Federico},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2021.3},
  URN =		{urn:nbn:de:0030-drops-148721},
  doi =		{10.4230/OASIcs.ATMOS.2021.3},
  annote =	{Keywords: Public Transportation, Timetabling, Machine Learning, Robustness}
}
Document
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
Robustness as a Third Dimension for Evaluating Public Transport Plans

Authors: Markus Friedrich, Matthias Müller-Hannemann, Ralf Rückert, Alexander Schiewe, and Anita Schöbel

Published in: OASIcs, Volume 65, 18th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2018)


Abstract
Providing attractive and efficient public transport services is of crucial importance due to higher demands for mobility and the need to reduce air pollution and to save energy. The classical planning process in public transport tries to achieve a reasonable compromise between service quality for passengers and operating costs. Service quality mostly considers quantities like average travel time and number of transfers. Since daily public transport inevitably suffers from delays caused by random disturbances and disruptions, robustness also plays a crucial role. While there are recent attempts to achieve delay-resistant timetables, comparably little work has been done to systematically assess and to compare the robustness of transport plans from a passenger point of view. We here provide a general and flexible framework for evaluating public transport plans (lines, timetables, and vehicle schedules) in various ways. It enables planners to explore several trade-offs between operating costs, service quality (average perceived travel time of passengers), and robustness against delays. For such an assessment we develop several passenger-oriented robustness tests which can be instantiated with parameterized delay scenarios. Important features of our framework include detailed passenger flow models, delay propagation schemes and disposition strategies, rerouting strategies as well as vehicle capacities. To demonstrate possible use cases, our framework has been applied to a variety of public transport plans which have been created for the same given demand for an artificial urban grid network and to instances for long-distance train networks. As one application we study the impact of different strategies to improve the robustness of timetables by insertion of supplement times. We also show that the framework can be used to optimize waiting strategies in delay management.

Cite as

Markus Friedrich, Matthias Müller-Hannemann, Ralf Rückert, Alexander Schiewe, and Anita Schöbel. Robustness as a Third Dimension for Evaluating Public Transport Plans. In 18th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2018). Open Access Series in Informatics (OASIcs), Volume 65, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{friedrich_et_al:OASIcs.ATMOS.2018.4,
  author =	{Friedrich, Markus and M\"{u}ller-Hannemann, Matthias and R\"{u}ckert, Ralf and Schiewe, Alexander and Sch\"{o}bel, Anita},
  title =	{{Robustness as a Third Dimension for Evaluating Public Transport Plans}},
  booktitle =	{18th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2018)},
  pages =	{4:1--4:17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-096-5},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{65},
  editor =	{Bornd\"{o}rfer, Ralf and Storandt, Sabine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2018.4},
  URN =		{urn:nbn:de:0030-drops-97097},
  doi =		{10.4230/OASIcs.ATMOS.2018.4},
  annote =	{Keywords: robustness, timetabling, vehicle schedules, delays}
}
Document
Robustness Tests for Public Transport Planning

Authors: Markus Friedrich, Matthias Müller-Hannemann, Ralf Rückert, Alexander Schiewe, and Anita Schöbel

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


Abstract
The classical planning process in public transport planning focuses on the two criteria operating costs and quality for passengers. Quality mostly considers quantities like average travel time and number of transfers. Since public transport often suffers from delays caused by random disturbances, we are interested in adding a third dimension: robustness. We propose passenger-oriented robustness indicators for public transport networks and timetables. These robustness indicators are evaluated for several public transport plans which have been created for an artificial urban network with the same demand. The study shows that these indicators are suitable to measure the robustness of a line plan and a timetable. We explore different trade-offs between operating costs, quality (average travel time of passengers), and robustness against delays. Our results show that the proposed robustness indicators give reasonable results.

Cite as

Markus Friedrich, Matthias Müller-Hannemann, Ralf Rückert, Alexander Schiewe, and Anita Schöbel. Robustness Tests for Public Transport Planning. In 17th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2017). Open Access Series in Informatics (OASIcs), Volume 59, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{friedrich_et_al:OASIcs.ATMOS.2017.6,
  author =	{Friedrich, Markus and M\"{u}ller-Hannemann, Matthias and R\"{u}ckert, Ralf and Schiewe, Alexander and Sch\"{o}bel, Anita},
  title =	{{Robustness Tests for Public Transport Planning}},
  booktitle =	{17th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2017)},
  pages =	{6:1--6:16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-042-2},
  ISSN =	{2190-6807},
  year =	{2017},
  volume =	{59},
  editor =	{D'Angelo, Gianlorenzo and Dollevoet, Twan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2017.6},
  URN =		{urn:nbn:de:0030-drops-78904},
  doi =		{10.4230/OASIcs.ATMOS.2017.6},
  annote =	{Keywords: robustness measure, timetabling, line planning, delays, passenger-orientation}
}
Document
10461 Abstracts Collection and Summary – Schematization in Cartography, Visualization, and Computational Geometry

Authors: Jason Dykes, Matthias Müller-Hannemann, and Alexander Wolff

Published in: Dagstuhl Seminar Proceedings, Volume 10461, Schematization in Cartography, Visualization, and Computational Geometry (2011)


Abstract
The Dagstuhl Seminar 10461 ``Schematization in Cartography, Visualization, and Computational Geometry'' was held November 14--19, 2010 in Schloss Dagstuhl~-- Leibniz Center for Informatics. The seminar brought together experts from the areas graph drawing, information visualization, geographic information science, computational geometry, very-large-scale integrated circuit (VLSI) layout, and underground mining. The aim was to discuss problems that arise when computing the layout of complex networks under angular restrictions (that govern the way in which the network edges are drawn). This collection consists of abstracts of three different types of contributions that reflect the different stages of the seminar; (a)~survey talks about the role of schematization in the various communities represented at the seminar, (b)~talks in the open problem and open mic sessions, and (c)~introductory talks.

Cite as

Jason Dykes, Matthias Müller-Hannemann, and Alexander Wolff. 10461 Abstracts Collection and Summary – Schematization in Cartography, Visualization, and Computational Geometry. In Schematization in Cartography, Visualization, and Computational Geometry. Dagstuhl Seminar Proceedings, Volume 10461, pp. 1-36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{dykes_et_al:DagSemProc.10461.1,
  author =	{Dykes, Jason and M\"{u}ller-Hannemann, Matthias and Wolff, Alexander},
  title =	{{10461 Abstracts Collection and Summary – Schematization in Cartography, Visualization, and Computational Geometry}},
  booktitle =	{Schematization in Cartography, Visualization, and Computational Geometry},
  pages =	{1--36},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2011},
  volume =	{10461},
  editor =	{Jason Dykes and Mattias M\"{u}ller-Hannemann and Alexander Wolff},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10461.1},
  URN =		{urn:nbn:de:0030-drops-30859},
  doi =		{10.4230/DagSemProc.10461.1},
  annote =	{Keywords: Information visualization, geo-visualization, geographic information systems, cartography, graph drawing, VLSI layout, underground mining, cartographic generalization, schematization, building simplification, orthogonal graph drawing, octilinear layout, schematic maps, Steiner trees}
}
Document
FORTES: Forensic Information Flow Analysis of Business Processes

Authors: Rafael Accorsi and Günter Müller

Published in: Dagstuhl Seminar Proceedings, Volume 10141, Distributed Usage Control (2010)


Abstract
Nearly 70% of all business processes in use today rely on automated workflow systems for their execution. Despite the growing expenses in the design of advanced tools for secure and compliant deployment of workflows, an exponential growth of dependability incidents persists. Concepts beyond access control focusing on information flow control offer new paradigms to design security mechanisms for reliable and secure IT-based workflows. This talk presents FORTES, an approach for the forensic analysis of information flow properties. FORTES claims that information flow control can be made usable as a core of an audit-control system. For this purpose, it reconstructs workflow models from secure log files (i.e. execution traces) and, applying security policies, analyzes the information flows to distinguish security relevant from security irrelevant information flows. FORTES thus cannot prevent security policy violations, but by detecting them with well-founded analysis, improve the precision of audit controls and the generated certificates.

Cite as

Rafael Accorsi and Günter Müller. FORTES: Forensic Information Flow Analysis of Business Processes. In Distributed Usage Control. Dagstuhl Seminar Proceedings, Volume 10141, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{accorsi_et_al:DagSemProc.10141.4,
  author =	{Accorsi, Rafael and M\"{u}ller, G\"{u}nter},
  title =	{{FORTES: Forensic Information Flow Analysis of Business Processes}},
  booktitle =	{Distributed Usage Control},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10141},
  editor =	{Sandro Etalle and Alexander Pretschner and Raiv S. Sandhu and Marianne Winslett},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10141.4},
  URN =		{urn:nbn:de:0030-drops-27167},
  doi =		{10.4230/DagSemProc.10141.4},
  annote =	{Keywords: Audit, Information flow analysis, business processes}
}
Document
Solving hard instances in QF-BV combining Boolean reasoning with computer algebra

Authors: Markus Wedler, Evgeny Pavlenko, Alexander Dreyer, Frank Seelisch, Dominik Stoffel, Gert-Martin Greuel, and Wolfgang Kunz

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


Abstract
This paper describes our new satisfyability (SAT) modulo theory (SMT) solver STABLE for the quantifier-free logic over fixed size bit vectors. Our main application domain is formal verification of system-on-chip (SoC) modules designed for complex computational tasks, for example, in signal processing applications. Ensuring proper functional behavior for such modules, including arithmetic correctness of the data paths, is considered a very difficult problem. We show how methods from computer algebra can be integrated into an SMT solver such that instances can be handled where the arithmetic problem parts are specified mixing various levels of abstraction from the plain gate level for small highly optimized components up to the pure word level used in high-level specifications. If the arithmetic problem parts include multiplications such mixed problem descriptions quickly drive current SMT solvers towards their capacity limits. High performance data paths are often designed at a level of abstraction that we call the arithmetic bit level (ABL). We show how ABL information, if available in an SMT instance, can be used to transform the decision problem into an equivalent set of variety subset problems. These problems can be solved efficiently with techniques from computer algebra based on Gröbner basis theory over finite rings Z/2^n . Sometimes, instances contain problem parts at a level below the ABL using gate-level operations. These problem parts, e.g., originate from custom-designed arithmetic components that are highly optimized using the gate-level constructs of a hardware description language (HDL). For such cases we integrate a local ABL extraction technique based on local Reed-Muller forms.

Cite as

Markus Wedler, Evgeny Pavlenko, Alexander Dreyer, Frank Seelisch, Dominik Stoffel, Gert-Martin Greuel, and Wolfgang Kunz. Solving hard instances in QF-BV combining Boolean reasoning with computer algebra. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{wedler_et_al:DagSemProc.09461.4,
  author =	{Wedler, Markus and Pavlenko, Evgeny and Dreyer, Alexander and Seelisch, Frank and Stoffel, Dominik and Greuel, Gert-Martin and Kunz, Wolfgang},
  title =	{{Solving hard instances in QF-BV combining Boolean reasoning with computer algebra}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--20},
  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-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.4},
  URN =		{urn:nbn:de:0030-drops-25096},
  doi =		{10.4230/DagSemProc.09461.4},
  annote =	{Keywords: SAT modulo Theory, Quantifier Free logic over fixed sized bitvectors; Computer Algebra}
}
Document
A Unified Framework for Verification Techniques for Object Invariants

Authors: Sophia Drossopoulou, Adrian Francalanza, P. Müller, and Alexander J. Summers

Published in: Dagstuhl Seminar Proceedings, Volume 8061, Types, Logics and Semantics for State (2008)


Abstract
Object invariants define the consistency of objects. They have subtle semantics, mainly because of call-backs, multi-object invariants, and subclassing. Several verification techniques for object invariants have been proposed. It is difficult to compare these techniques, and to ascertain their soundness, because of their differences in restrictions on programs and invariants, in the use of advanced type systems (e.g., ownership types), in the meaning of invariants, and in proof obligations. We develop a unified framework for such techniques. We distil seven parameters that characterise a verification technique, and identify sufficient conditions on these parameters which guarantee soundness. We instantiate our framework with three verification techniques from the literature, and use it to assess soundness and compare expressiveness.

Cite as

Sophia Drossopoulou, Adrian Francalanza, P. Müller, and Alexander J. Summers. A Unified Framework for Verification Techniques for Object Invariants. In Types, Logics and Semantics for State. Dagstuhl Seminar Proceedings, Volume 8061, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{drossopoulou_et_al:DagSemProc.08061.3,
  author =	{Drossopoulou, Sophia and Francalanza, Adrian and M\"{u}ller, P. and Summers, Alexander J.},
  title =	{{A Unified Framework for  Verification Techniques for Object Invariants}},
  booktitle =	{Types, Logics and Semantics for State},
  pages =	{1--25},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8061},
  editor =	{Amal Ahmed and Nick Benton and Martin Hofmann and Greg Morrisett},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08061.3},
  URN =		{urn:nbn:de:0030-drops-14278},
  doi =		{10.4230/DagSemProc.08061.3},
  annote =	{Keywords: Object invariants, visible states semantics, verification, sound}
}
  • Refine by Author
  • 4 Müller-Hannemann, Matthias
  • 3 Rückert, Ralf
  • 3 Schiewe, Alexander
  • 3 Schöbel, Anita
  • 2 Friedrich, Markus
  • Show More...

  • Refine by Classification
  • 2 Applied computing → Transportation
  • 1 Applied computing → Sound and music computing
  • 1 Computer systems organization → Quantum computing
  • 1 Hardware → Quantum error correction and fault tolerance
  • 1 Information systems → Music retrieval
  • Show More...

  • Refine by Keyword
  • 2 delays
  • 2 timetabling
  • 1 Audio signal processing
  • 1 Audit
  • 1 Clifford hierarchy
  • Show More...

  • Refine by Type
  • 10 document

  • Refine by Publication Year
  • 2 2010
  • 2 2022
  • 1 2008
  • 1 2011
  • 1 2017
  • 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