Rechnerarchitektur - Universität Freiburg

Name	Tobias Schubert, Dr.
Adresse	Technische Fakultät Albert-Ludwigs-Universität Georges Köhler Allee, Gebäude 51 79110 Freiburg im Breisgau Deutschland
Büro	Gebäude 51, Raum 01..033
Telefon	++49 +761 203-8153
Fax	++49 +761 203-8142
eMail	schubert@informatik.uni-freiburg.de

Tobias Schubert

Jahre: 2017 | 2016 | 2015 | 2014 | 2013 | 2012 | 2011 | 2010 | 2009 | 2007 | 2006 | 2005 | 2004 | 2003 | 2000

2017

nach oben zur Jahresübersicht

Isabel Dahlhausen, Tobias Schubert
Von der Teilnehmendenanalyse zur lernförderlichen Gestaltung: Wie können wir E-Learning lebendiger machen?
2017 16. Internationale ILIAS-Konferenz
Jan Burchard, Maël Gay, Ange-Salomé Messeng Ekossono, Jan Horáček, Bernd Becker, Tobias Schubert, Martin Kreuzer, Ilia Polian
Attacks
2017 Fault Diagnosis and Tolerance in Cryptography (FDTC) 2017
KurzfassungA prototype of the framework AutoFault, which automatically constructs fault-injection attacks for hardware realizations of ciphers, is presented. AutoFault can be used to quickly evaluate the resistance of security-critical hardware blocks to fault attacks and the adequacy of implemented countermeasures. The framework takes as inputs solely the circuit description of the cipher and the fault(s) and produces an algebraic formula that can be handed over to an external solver. In contrast to previous work, attacks constructed by AutoFault do not incorporate any cipher-specific cryptoanalytic derivations, making the framework accessible to users without cryptographic background. We report successful application of AutoFault in combination with a state-of-the-art SAT solver to LED-64 and to small-scale AES. To the best of our knowledge, this is the first time that a state-of-the-art cipher (LED-64) was broken by a fault attack with no prior manual cryptanalysis whatsoever.
Jan Burchard, Ange-Salomé Messeng Ekossono, Jan Horáček, Maël Gay, Bernd Becker, Tobias Schubert, Martin Kreuzer, Ilia Polian
Algebraic Fault Attacks on Ciphers
2017 RESCUE Workshop on Reliability, Security and Quality at ETS 2017
Jan Burchard, Ange-Salomé Messeng Ekossono, Jan Horáček, Maël Gay, Bernd Becker, Tobias Schubert, Martin Kreuzer, Ilia Polian
Algebraic Fault Attacks on Ciphers
2017 International Verification and Security Workshop (IVSW) 2017
Tobias Schubert, Benjamin Völker, Marc Pfeifer, Bernd Becker
The Smart MiniFab: An Industrial IoT Demonstrator Anywhere at Any Time
2017 Smart Education and e-Learning 2017, Vilamoura/Portugal, KES International Springer International Publishing, Seiten: 253 - 262

2016

nach oben zur Jahresübersicht

Marc Pfeifer, Tobias Schubert, Bernd Becker
PackSens: A Condition and Transport Monitoring System Based on an Embedded Sensor Platform
2016 7th EAI International Conference on Sensor Systems and Software Proceedings of the 7th EAI International Conference on Sensor Systems and Software, Seiten: 81 - 92
KurzfassungAs a consequence of the growing globalization, transports which need a safe handling are increasing. Therefore, this paper introduces an innovative transport and condition monitoring system based on a mobile embedded sensor platform. The platform is equipped with a variety of sensors needed to extensively monitor a transport and can be attached directly to the transported good. The included microcontroller processes all relevant data served by the sensors in a very power efficient manner. Furthermore, it provides possible violations of previously given thresholds through a standardized Near Field Communication (NFC) interface to the user. Since falls are one major cause of damages while transportation, the presented system is the first one that not only detects every fall but also analyses the fall height and other parameters related to the fall event in real-time on the platform. The whole system was tested in different experiments where all critical situations and in particular all fall situations have been detected correctly.
Benjamin Völker, Tobias Schubert, Bernd Becker
iHouse: A Voice-Controlled, Centralized, Retrospective Smart Home
2016 7th EAI International Conference on Sensor Systems and Software
KurzfassungSpeech recognition in smart home systems has become pop- ular in both, research and consumer areas. This paper introduces an in- novative concept for a modular, customizable, and voice-controlled smart home system. The system combines the advantages of distributed and centralized processing to enable a secure as well as highly modular plat- form and allows to add existing non-smart components retrospectively into the smart environment. To interact with the system in the most com- fortable way - and in particular without additional devices like smart- phones - voice-controlling was added as the means of choice. The task of speech recognition is partitioned into decentral Wake-Up-Word (WUW) recognition and central continuous speech recognition to enable flexibil- ity while maintaining security. This is achieved utilizing a novel WUW algorithm suitable to be executed on small microcontrollers which uses Mel Frequency Cepstral Coefficients as well as Dynamic Time Warping. A high rejection rate up to 99.93% was achieved, justifying the use of the algorithm as a voice trigger in the developed smart home system.
Tobias Schubert, Isabel Dahlhausen
Bereich Industrie 4.0
2016 DGWF-Jahrestagung 2016, Seiten: 142 - 143
Jan Burchard, Tobias Schubert, Bernd Becker
Distributed Parallel #SAT Solving
2016 IEEE Cluster 2016
Kurzfassungof available cores dCountAntom solved problems on average 141 times faster than a single core implementation.
Maël Gay, Jan Burchard, Jan Horáček, Ange-Salomé Messeng Ekossono, Tobias Schubert, Bernd Becker, Ilia Polian, Martin Kreuzer
Formulas, Circuit-Implementations and Fault Equations
2016 FCTRU'16

2015

nach oben zur Jahresübersicht

Jan Burchard, Tobias Schubert, Bernd Becker
Laissez-Faire Caching for Parallel #SAT Solving
2015 International Conference on Theory and Applications of Satisfiability Testing, Band: 9340, Seiten: 46 - 61
Kurzfassungcaching only adds a small computational overhead.
Katrin Weber, Corinna Bertuzzi, Tobias Schubert
Kooperation in der virtuellen Projektarbeit – Vom Pilotkurs zum erfolgreichen Weiterbildungsangebot in den Technikwissenschaften
2015 DGWF-Jahrestagung 2015, Seiten: 144 - 145
Linus Feiten, Matthias Sauer, Tobias Schubert, Victor Tomashevich, Ilia Polian, Bernd Becker
Formal Vulnerability Analysis of Security Components
2015 IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), Band: 34, Nummer: 8, Seiten: 1358 - 1369
KurzfassungVulnerability to malicious fault attacks is an emerging concern for hardware circuits that are employed in mobile and embedded systems and process sensitive data. We describe a new methodology to assess the vulnerability of a circuit to such attacks, taking into account built-in protection mechanisms. Our method is based on accurate modeling of fault effects and detection status expressed by Boolean satisfiability (SAT) formulas. Vulnerability is quantified based on the number of solutions of these formulas, which are determined by an efficient #SAT solver. We demonstrate the applicability of this method for design space exploration of a pseudo random number generator and for calculating the attack success rate in a multiplier circuit protected by robust error-detecting codes.

2014

nach oben zur Jahresübersicht

Sven Reimer, Matthias Sauer, Tobias Schubert, Bernd Becker
Incremental Encoding and Solving of Cardinality Constraints
2014 International Symposium on Automated Technology for Verification and Analysis, Springer International Publishing, Band: 8837, Seiten: 297 - 313
KurzfassungTraditional SAT-based MaxSAT solvers encode cardinality constraints directly as part of the CNF and solve the entire optimization problem by a sequence of iterative calls of the underlying SAT solver. The main drawback of such approaches is their dependence on the number of soft clauses: The more soft clauses the MaxSAT instance contains, the larger is the CNF part encoding the cardinality constraints. To counter this drawback, we introduce an innovative encoding of cardinality constraints: Instead of translating the entire and probably bloated constraint network into CNF, a divide-and-conquer approach is used to encode partial constraint networks successively. The resulting subproblems are solved and merged incrementally, reusing not only intermediate local optima, but also additional constraints which are derived from solving the individual subproblems by the back-end SAT solver. Extensive experimental results for the last MaxSAT evaluation benchmark suitew demonstrate that our encoding is in general smaller compared to existing methods using a monolithic encoding of the constraints and converges faster to the global optimum.
Tobias Schubert, Marc Pfeifer, Bernd Becker
Accurate Controlling of Velocity on a Mobile Robot
2014 29th International Conference on Computers and Their Applications
Dominik Erb, Michael Koche, Matthias Sauer, Stefan Hillebrecht, Tobias Schubert, Hans-Joachim Wunderlich, Bernd Becker
Exact Logic and Fault Simulation in Presence of Unknowns
2014 ACM Transactions on Design Automation of Electronic Systems (TODAES), Band: 19, Seiten: 28:1 - 28:17
Kurzfassungsignificantly increased without increasing the test set size.
Linus Feiten, Andreas Spilla, Matthias Sauer, Tobias Schubert, Bernd Becker
Implementation and Analysis of Ring Oscillator PUFs on 60 nm Altera Cyclone FPGAs
2014 Information Security Journal: A Global Perspective, Band: 22, Nummer: 5-6, Seiten: 265 - 273
KurzfassungRing Oscillator (RO) physically unclonable functions (PUFs) on field programmable gate arrays (FPGAs) have drawn much attention in recent years. Making each FPGA uniquely identifiable, they allow for protection of intellectual property (IP) or generation of secret encryption keys. Their implementation has been widely discussed, but most experiments have been conducted on Xilinx platforms. In this paper, we report the statistical results from an analysis spanning 20 Cyclone IV FPGAs with 60 nm technology. We parameterize the RO length, placement, ambient temperature, and non-PUF switching activity and discuss the observed effects on PUF quality.
Sven Reimer, Matthias Sauer, Tobias Schubert, Bernd Becker
Using MaxBMC for Pareto-Optimal Circuit Initialization
2014 Conf. on Design, Automation and Test in Europe
KurzfassungIn this paper we present MaxBMC, a novel formalism for solving optimization problems in sequential systems. Our approach combines techniques from symbolic SAT-based Bounded Model Checking (BMC) and incremental MaxSAT, leading to the first MaxBMC solver. In traditional BMC safety and liveness properties are validated. We extend this formalism: in case the required property is satisfied, an optimization problem is defined to maximize the quality of the reached witnesses. Further, we compare its qualities in different depths of the system, leading to Pareto-optimal solutions. We state a sound and complete algorithm that not only tackles the optimization problem but moreover verifies whether a global optimum has been identified by using a complete BMC solver as back-end. As a first reference application we present the problem of circuit initialization. Additionally, we give pointers to other tasks which can be covered by our formalism quite naturally and further demonstrate the efficiency and effectiveness of our approach.

2013

nach oben zur Jahresübersicht

Tobias Schubert, Jan Burchard, Matthias Sauer, Bernd Becker
S-Trike: A Mobile Robot Platform for Higher Education
2013 International Conference on Computer Applications in Industry and Engineering, Seiten: 243 - 248
Linus Feiten, Andreas Spilla, Matthias Sauer, Tobias Schubert, Bernd Becker
Analysis of Ring Oscillator PUFs on 60nm FPGAs
2013 TRUDEVICE Workshop, Avignon
KurzfassungThe implementation of RO PUFs on FPGAs has been widely discussed but most experiments have been conducted on Xilinx FPGAs. In this paper we are reporting statistical results from an analysis spanning 20 equivalent Altera FPGAs. The presented results include the PUF quality's dependency on different parameters like RO length and placement on the FPGA. We identify the optimal RO length of 16 Logic Elements (LE) and show some specific placement cases for which the otherwise very good PUF quality decreases drastically.
Linus Feiten, Matthias Sauer, Tobias Schubert, Alexander Czutro, Victor Tomashevich, Eberhard Böhl, Ilia Polian, Bernd Becker
#SAT for Vulnerability Analysis of Security Components
2013 (Workshop-Paper, Informal Proceedings) IEEE European Test Symposium
KurzfassungVulnerability to malicious fault attacks is an emerging concern for hardware circuits that process sensitive data.We describe a new methodology to assess the vulnerability to such attacks, taking into account built-in protection mechanisms. Our method is based on accurate modeling of fault effects and their detection status expressed as Boolean satisfiability (SAT) formulae. Vulnerability is quantified based on the number of solutions of such formulae, which are computed by an eficient #SAT solver. We demonstrate the applicability of this method by analyzing a sequential pseudo random number generator and a combinatorial multiplier circuit both protected by robust error-detecting codes.
Benjamin Andres, Matthias Sauer, Martin Gebser, Tobias Schubert, Bernd Becker, Torsten Schaub
Accurate Computation of Sensitizable Paths using Answer Set Programming
2013 Int. Conf. on Logic Programming and Nonmonotonic Reasoning, Seiten: 92 - 101
KurzfassungPrecise knowledge of the longest sensitizable paths in a circuit is crucial for various tasks in computer-aided design, including timing analysis, performance optimization, delay testing, and speed binning. As delays in today’s nanoscale technologies are increasingly affected by statistical parameter variations, there is significant interest in obtaining sets of paths that are within a length range. For instance, such path sets can be used in the emerging areas of Post-silicon validation and characterization and Adaptive Test. We present an ASP-based method for computing well-defined sets of sensitizable paths within a length range. Unlike previous approaches, the method is accurate and does not rely on a priori relaxations. Experimental results demonstrate the applicability and scalability of our method.
Matthias Sauer, Sven Reimer, Stefan Kupferschmid, Tobias Schubert, Paolo Marin, Bernd Becker
Applying BMC, Craig Interpolation and MAX-SAT to Functional Justification in Sequential Circuits
2013 RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
Kurzfassungsuch sequences depending on the number of controllable ﬂip-ﬂops.
Matthias Sauer, Sven Reimer, Tobias Schubert, Ilia Polian, Bernd Becker
Efficient SAT-Based Dynamic Compaction and Relaxation for Longest Sensitizable Paths
2013 Conf. on Design, Automation and Test in Europe, Seiten: 448 - 453
KurzfassungComprehensive coverage of small-delay faults under massive process variations is achieved when multiple paths through the fault locations are sensitized by the test pair set. Using one test pair per path may lead to impractical test set sizes and test application times due to the large number of near-critical paths in state-of-the-art circuits.
Matthias Sauer, Sven Reimer, Ilia Polian, Tobias Schubert, Bernd Becker
Provably Optimal Test Cube Generation Using Quantified Boolean Formula Solving
2013 ASP Design Automation Conf.
KurzfassungCircuits that employ test pattern compression rely on test cubes to achieve high compression ratios. The less inputs of a test pattern are specified, the better it can be compacted and hence the lower the test application time. Although there exist previous approaches to generate such test cubes, none of them are optimal. We present for the first time a framework that yields provably optimal test cubes by using the theory of quantified Boolean formulas (QBF). Extensive comparisons with previous methods demonstrate the quality gain of the proposed method.
Matthias Sauer, Alexander Czutro, Tobias Schubert, Stefan Hillebrecht, Ilia Polian, Bernd Becker
SAT-based Analysis of Sensitisable Paths
2013 Test of Computers, Band: 30, Nummer: 4, Seiten: 81 - 88
KurzfassungA common trend in the past has been to detect delay defects in nanoscale technologies through the longest sensitisable paths. This approach does not hold up for non-trivial defects due to modeling inaccuracies. This article supports tests through all paths of customized length, using current SAT-solving advances.
Matthias Sauer, Jan Burchard, Tobias Schubert, Ilia Polian, Bernd Becker
Waveform-Guided Fault Injection by Clock Manipulation
2013 TRUDEVICE Workshop

2012

nach oben zur Jahresübersicht

Linus Feiten, Matthias Sauer, Tobias Schubert, Alexander Czutro, Eberhard Böhl, Ilia Polian, Bernd Becker
#SAT-Based Vulnerability Analysis of Security Components -- A Case Study
2012 IEEE International Symposium on Defect and Fault Tolerance (DFT), Seiten: 49 - 54
KurzfassungIn this paper we describe a new approach to assess a circuit's vulnerability to fault attacks. This is achieved through analysis of the circuit's design specification, making use of modern SAT solving techniques. For each injectable fault, a corresponding SAT instance is generated. Every satisfying solution for such an instance is equivalent to a circuit state and an input assignment for which the fault affcts the circuit's outputs such that the error is not detected by the embedded fault detection. The number of solutions is precisely calculated by a #SAT solver and can be translated into an exact vulnerability measure. We demonstrate the applicability of this method for design space exploration by giving detailed results for various implementations of a deterministic random bit generator.
Benjamin Andres, Matthias Sauer, Martin Gebser, Tobias Schubert, Bernd Becker, Torsten Schaub
Accurate Computation of Longest Sensitizable Paths using Answer Set Programming
2012 GMM/ITG-Fachtagung “Zuverlässigkeit und Entwurf”
Alexander Czutro, Matthias Sauer, Tobias Schubert, Ilia Polian, Bernd Becker
SAT-ATPG Using Preferences for Improved Detection of Complex Defect Mechanisms
2012 VLSI Test Symp.
KurzfassungFailures caused by phenomena such as crosstalk or power-supply noise are gaining in importance in advanced nanoscale technologies. The detection of such complex defects benefits from the satisfaction of certain constraints, for instance justifying specific transitions on neighbouring lines of the defect location. We present a SAT-based ATPG-tool that supports the enhanced conditional multiple-stuck-at fault model (ECMS@). This model can specify multiple fault locations along with a set of hard conditions imposed on arbitrary lines; hard conditions must hold in order for the fault effect to become active. Additionally, optimisation constraints that may be required for best coverage can be specified via a set of soft conditions. The introduced tool justifies as many of these conditions as possible, using a mechanism known as SAT with preferences. Several applications are discussed and evaluated by extensive experimental data. Furthermore, a novel fault-clustering technique is introduced, thanks to which the time required to classify all stuck-at faults in a suite of industrial benchmarks was reduced by up to 65%.

2011

nach oben zur Jahresübersicht

Stefan Kupferschmid, Matthew Lewis, Tobias Schubert, Bernd Becker
Incremental preprocessing methods for use in BMC
2011 Formal Methods in System Design, Band: 39, Seiten: 185 - 204
Kurzfassung. Unfortunately, many preprocessing techniques such as variable and (blocked) clause elimination cannot be directly used in an incremental manner. This work focuses on extending these techniques and Craig interpolation so that they can be used effectively together in incremental SAT solving (in the context of BMC). The techniques introduced here doubled the performance of our BMC solver on both SAT and UNSAT problems. For UNSAT problems, preprocessing had the added advantage that Craig interpolation was able to find the fixed point sooner, reducing the number of incremental SAT iterations. Furthermore, our ideas seem to perform better as the benchmarks become larger, and/or deeper, which is exactly when they are needed. Lastly, our methods can be integrated into other SAT based BMC tools to achieve similar speedups.
Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico Giunchiglia
Parallel QBF Solving with Advanced Knowledge Sharing
2011 Fundamenta Informaticae, Band: 107, Nummer: 2-3, Seiten: 139 - 166
KurzfassungIn this paper we present the parallel QBF Solver PaQuBE. This new solver leverages the additional computational power that can be exploited from modern computer architectures, from pervasive multi-core boxes to clusters and grids, to solve more relevant instances faster than previous generation solvers. Furthermore, PaQuBE's progressive MPI based parallel framework is the first to support advanced knowledge sharing in which solution cubes as well as conflict clauses can be exchanged between solvers. Knowledge sharing plays a critical role in the performance of PaQuBE. However, due to the overhead associated with sending and receiving MPI messages, and the restricted communication/network bandwidth available between solvers, it is essential to optimize not only what information is shared, but the way in which it is shared. In this context, we compare multiple conflict clause and solution cube sharing strategies, and finally show that an adaptive method provides the best overall results.
Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, Christian Herde
Parallel SAT Solving in Bounded Model Checking
2011 Journal of Logic and Computation, Band: 21, Nummer: 1, Seiten: 5 - 21
KurzfassungBounded model checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver. We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths. We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting. We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results.
Matthias Sauer, Alexander Czutro, Tobias Schubert, Stefan Hillebrecht, Ilia Polian, Bernd Becker
SAT-Based Analysis of Sensitisable Paths
2011 IEEE Design and Diagnostics of Electronic Circuits and Systems, Seiten: 93 - 98
KurzfassungManufacturing defects in nanoscale technologies have highly complex timing behaviour that is also affected by process variations. While conventional wisdom suggests that it is optimal to detect a delay defect through the longest sensitisable path, non-trivial defect behaviour along with modelling inaccuracies necessitate consideration of paths of well-controlled length during test generation. We present a generic methodology that yields tests through all sensitisable paths of user-specified length. The resulting tests can be employed within the framework of adaptive testing. The methodology is based on encoding the problem as a Boolean-satisfiability (SAT) instance and thereby leverages recent advances in SAT-solving technology.

2010

nach oben zur Jahresübersicht

Stefan Kupferschmid, Matthew Lewis, Tobias Schubert, Bernd Becker
Incremental Preprocessing Methods for use in BMC
2010 Int'l Workshop on Hardware Verification
KurzfassungTraditional incremental SAT solvers have achieved great success in the domain of Bounded Model Checking (BMC). However, modern solvers depend on advanced preprocessing procedures to obtain high levels of performance. Unfortunately,many preprocessing techniques such as a variable and (blocked) clauseelimination cannot be directly used in an incremental manner. This work focuses on extending these techniques and Craig interpolation so that they can be used effectively together in incremental SAT solving (in the context of BMC). The techniques introduced here doubled the performance of our BMC solver onboth SAT and UNSAT problems. For UNSAT problems, preprocessing had the added advantagethat Craig interpolation was able to find the fixed point sooner,reducing the number of incremental SAT iterations. Furthermore, our ideas seem to perform better as the benchmarks become larger, and/or deeper, which is exactly when they are needed. Lastly, our methods can be extended to other SAT based BMC tools to achieve similar speedups.
Natalia Kalinnik, Erika Ábrahám, Tobias Schubert, Ralf Wimmer, Bernd Becker
Exploiting Different Strategies for the Parallelization of an SMT Solver
2010 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Fraunhofer Verlag, Seiten: 97 - 106
KurzfassungIn this paper we present two different parallelization schemes for the SMT solver iSAT, based on (1) the distribution of work by dividing the search space into disjoint parts and exploring them in parallel, thereby exchanging learnt information, and (2) a portfolio approach, where the entire benchmark instance isexplored in parallel by several copies of the same solver but usingdifferent heuristics to guide the search. We also combine bothapproaches such that solvers examine disjoint parts of the searchspace using different heuristics. The main contribution of the paper is to study the performances of different techniques for parallelizing iSAT.

2009

nach oben zur Jahresübersicht

Natalia Kalinnik, Tobias Schubert, Erika Ábrahám, Ralf Wimmer, Bernd Becker
Picoso - A Parallel Interval Constraint Solver
2009 Int'l Conf. on Parallel and Distributed Processing Techniques and Applications, CSREA Press, Seiten: 473 - 479
KurzfassungThis paper describes the parallel interval constraint solver Picoso, which can decide (a subclass of) boolean combinations of linear and non-linear constraints. Picoso follows a master/client model based on message passing, making it suitable for any kind of workstation cluster as well as for multi-processor machines. To run several clients in parallel, an efficient work stealing mechanism has been integrated, dividing the overall search space into disjoint parts. Additionally, to prevent the clients from running into identical conflicts, information about conflicts in form of conflict clauses is exchanged among the clients. Performance measurements, using four clients to solve a number of benchmark problems, show that Picoso yields linear speedup compared to the sequential interval constraint solver iSAT, on which the clients of Picoso are based.
Paolo Marin, Matthew Lewis, Massimo Narizzano, Tobias Schubert, Enrico Giunchiglia, Bernd Becker
Comparison of Knowledge Sharing Strategies in a Parallel QBF Solver
2009 High-Performance Computing and Simulation Conference, Seiten: 161 - 167
Matthew Lewis, Tobias Schubert, Bernd Becker
DPLL-based Reasoning in a Multi-Core Environment
2009 Int'l Workshop on Microprocessor Test and Verification
Paolo Marin, Matthew Lewis, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico Giunchiglia
Evaluation of Knowledge Sharing Strategies in a Parallel QBF Solver
2009 RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
Tobias Schubert, Matthew Lewis, Bernd Becker
PaMiraXT: Parallel SAT Solving with Threads and Message Passing
2009 Journal on Satisfiability, Boolean Modeling, and Computation, Band: 6, Seiten: 203 - 222
Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico Giunchiglia
PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing
2009 Int'l Conf. on Theory and Applications of Satisfiability Testing, Band: 5584, Seiten: 509 - 523
Matthew Lewis, Tobias Schubert, Bernd Becker
QMiraXT - A Multithreaded QBF Solver
2009 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”

2007

nach oben zur Jahresübersicht

Matthew Lewis, Tobias Schubert, Bernd Becker
Multithreaded SAT Solving
2007 ASP Design Automation Conf., Seiten: 926 - 921
Martin Fränzle, Christian Herde, Tino Teige, S. Ratschan, Tobias Schubert
Efficient Solving of Large Non-Linear Arithmetic Constraint Systems with Complex Boolean Structure
2007 Journal on Satisfiability, Boolean Modeling, and Computation, Band: 1, Nummer: 3-4, Seiten: 209 - 236

2006

nach oben zur Jahresübersicht

Martin Fränzle, Christian Herde, S. Ratschan, Tobias Schubert, Tino Teige
Interval Constraint Solving Using Propositional SAT Solving Techniques
2006 Int'l Workshop on the Integration of SAT and CP Techniques, Seiten: 81 - 95
Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, Christian Herde
Parallel SAT-Solving in Bounded Model Checking
2006 Int'l Workshop on Parallel and Distributed Methods in Verification, Springer-Verlag, Band: 4346, Seiten: 301 - 315
KurzfassungBounded Model Checking (BMC) is an incremental refutation technique to search for counterexamples of increasing length. The existence of a counterexample of a fixed length is expressed by a first-order logic formula that is checked for satisfiability using a suitable solver.We apply communicating parallel solvers to check satisfiability of the BMC formulae. In contrast to other parallel solving techniques, our method does not parallelize the satisfiability check of a single formula, but the parallel solvers work on formulae for different counterexample lengths. We adapt the method of constraint sharing and replication of Shtrichman, originally developed for sequential BMC, to the parallel setting. Since the learning mechanism is now parallelized, it is not obvious whether there is a benefit from the concepts of Shtrichman in the parallel setting. We demonstrate on a number of benchmarks that adequate communication between the parallel solvers yields the desired results.

2005

nach oben zur Jahresübersicht

Matthew Lewis, Tobias Schubert, Bernd Becker
Speedup Techniques Utilized in Modern SAT Solvers - An Analysis in the MIRA Environment
2005 Theory and Applications of Satisfiability Testing, Springer, Band: 3569, Seiten: 437 - 443
Kurzfassungs 28.
Tobias Schubert, Bernd Becker
A Hardware Lab Anywhere at Any Time
2005 Journal of Systemics, Cybernetics, and Informatics: JSCI, Band: 2, Nummer: 6
Tobias Schubert, Bernd Becker
Accelerating Boolean SAT Engines Using Hyper-Threading Technology
2005 Asian Applied Computing Conf.
Tobias Schubert, Bernd Becker
Knowledge Sharing in a Microcontroller based Parallel SAT Solver
2005 Int'l Conf. on Parallel and Distributed Processing Techniques and Applications
Tobias Schubert, Bernd Becker
Lemma Exchange in a Microcontroller based Parallel SAT Solver
2005 IEEE Int'l Symp. on VLSI
Tobias Schubert, Bernd Becker, Matthew Lewis
PaMira - A Parallel SAT Solver with Knowledge Sharing
2005 Int'l Workshop on Microprocessor Test and Verification, IEEE Computer Society, Band: 00, Seiten: 29 - 36
KurzfassungIn this paper we describe PaMira, a powerful distributed SAT solver. PaMira is based on the highly optimized, sequential SAT engine Mira, incorporating all essential optimization techniques modern algorithms utilize to maximize performance. For the distributed execution an efficient work stealing method has been implemented. PaMira also employs the exchange of conflict clauses between the processes to guide the search more efficiently. We provide experimental results showing linear speedup on a multiprocessor environment with four AMD Opteron processors.

2004

nach oben zur Jahresübersicht

Matthew Lewis, Tobias Schubert, Bernd Becker
Early Conflict Detection Based BCP for SAT Solving
2004 Int'l Conf. on Theory and Applications of Satisfiability Testing, Seiten: 29 - 36
KurzfassungAbstract. This paper describes a new BCP algorithm that improves the performance of Chaff class solvers by reducing the total number of clauses the BCP procedure must evaluate. This is done by: detecting conflicts earlier; evaluating clauses better; and by increasing the controllability of the conflicts which the BCP procedure finds. Solvers like Limmat [10] include a simple Early Conflict Detection BCP (ECDB), however we introduce a new aggressive ECDB procedure and the MIRA solver that efficiently incorporates it while easily facilitating comparisons between ECDB modes. With the full ECDB procedure enabled, MIRA was able to reduce the number of evaluated clauses by 59% on average compared to the disabled ECDB version. This new procedure and other speedup techniques discussed here allow MIRA to solve problems 3.7 times faster on average than zChaff. Lastly, this paper shows how significant speedup can be attained relatively easily by incorporating a certain level of ECDB into other solvers.
Tobias Schubert, Bernd Becker
A Distributed SAT Solver for Microchip Microcontroller
2004 Workshop on Parallel Systems and Algorithms
Matthew Lewis, Tobias Schubert, Bernd Becker
Early Conflict Detection Based SAT Solving
2004 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
Tobias Schubert, Bernd Becker
PICHAFF2 - A Hierarchical Parallel SAT Solver
2004 Int'l Workshop on Microprocessor Test and Verification
Tobias Schubert, Bernd Becker
Parallel SAT Solving with Microcontrollers
2004 Asian Applied Computing Conf.

2003

nach oben zur Jahresübersicht

Tobias Schubert, Bernd Becker
PICHAFF: A Distributed SAT Solver for Microcontrollers
2003 Euromicro Conf.
Tobias Schubert, Bernd Becker
A Hardware Lab Anywhere At Anytime
2003 Int'l Conf. on Education and Information Systems: Technologies and Applications, Seiten: 130 - 135
Andreas Hett, Tobias Schubert
A Hardware Lab in a Pocket
2003 World Conf. on E-Learning in Corporate, Government, Healthcare, and Higher Education
Tobias Schubert, Andreas Hett
A Hardware Lab in a Pocket
2003 Int'l Conf. on Multimedia and Information and Communication Technologies in Education
Tobias Schubert, Bernd Becker
Das Mobile Hardware-Praktikum
2003 European Conf. on Media in Higher Education

2000

nach oben zur Jahresübersicht

Rolf Drechsler, Nicole Drechsler, Elke Mackensen, Tobias Schubert, Bernd Becker
Design Reuse by Modularity: A Scalable Dynamical (Re)Configurable Multiprocessor System
2000 Euromicro Conf., Seiten: 1:425 - 431
Tobias Schubert, Elke Mackensen, Nicole Drechsler, Rolf Drechsler, Bernd Becker
Specialized Hardware for Implementation of Evolutionary Algorithms
2000 Int'l Workshop on Boolean Problems, Seiten: 175 - 182
Tobias Schubert, Elke Mackensen, Nicole Drechsler, Rolf Drechsler, Bernd Becker
Specialized Hardware for Implementation of Evolutionary Algorithms
2000 Conf. on Genetic and Evolutionary Computation, Seite: 369