Tobias Schubert, Dr.
Technische Fakultät Albert-Ludwigs-Universität Georges Köhler Allee, Gebäude 51 79110 Freiburg im Breisgau Deutschland
Gebäude 51, Raum 01..033
++49 +761 203-8153
++49 +761 203-8142
schubert@informatik.uni-freiburg.de
Tobias Schubert
Liste filtern : Jahre: 2017 |
2016 |
2015 |
2014 |
2013 |
2012 |
2011 |
2010 |
2009 |
2007 |
2006 |
2005 |
2004 |
2003 |
2000 | alle anzeigen nach oben zur Jahresübersicht Isabel Dahlhausen, Tobias SchubertVon 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 PolianAutoFault: Towards Automatic Construction of Algebraic Fault
Attacks 2017 Fault Diagnosis and Tolerance in Cryptography (FDTC) 2017 » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung A 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. Tobias Schubert, Benjamin Völker, Marc Pfeifer, Bernd BeckerThe 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 Jan Burchard, Ange-Salomé Messeng Ekossono, Jan Horáček, Maël Gay, Bernd Becker, Tobias Schubert, Martin Kreuzer, Ilia PolianTowards Mixed Structural-Functional Models for
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 PolianTowards Mixed Structural-Functional Models for
Algebraic Fault Attacks on Ciphers 2017 International Verification and Security Workshop (IVSW) 2017 nach oben zur Jahresübersicht Benjamin Völker, Tobias Schubert, Bernd BeckeriHouse: A Voice-Controlled, Centralized, Retrospective Smart Home 2016 7th EAI International Conference on Sensor Systems and Software » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Speech 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 DahlhausenPilotkurs Schlüsseltechnologien der vernetzten
Produktion – Wissenschaftliche Weiterbildung für
Ingenieure und Ingenieurinnen, Fach‐ & Führungskräfte im
Bereich Industrie 4.0 2016 DGWF-Jahrestagung 2016 , Seiten : 142 - 143 Jan Burchard, Tobias Schubert, Bernd BeckerDistributed Parallel #SAT Solving 2016 IEEE Cluster 2016 » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The #SAT problem, that is counting the number
of solutions of a propositional formula, extends the well-
known SAT problem into the realm of probabilistic reasoning.
However, the higher computational complexity and lack of fast
solvers still limits its applicability for real world problems.
In this work we present our distributed parallel #SAT solver
dCountAntom which utilizes both local, shared-memory paral-
lelism as well as distributed (cluster computing) parallelism.
Although highly parallel solvers are known in SAT solving,
such techniques have never been applied to the #SAT problem.
Furthermore we introduce a solve progress indicator which
helps the user to assess whether the presented problem is likely
solvable within a reasonable time. Our analysis shows a high
accuracy of the estimated progress.
Our experiments with up to 256 CPU cores working in
parallel yield large speedups across different benchmarks
derived from real world problems: With the maximum number
of available cores dCountAntom solved problems on average 141 times faster than a single core implementation. Marc Pfeifer, Tobias Schubert, Bernd BeckerPackSens: A Condition and Transport Monitoring System Based on an Embedded Sensor Platform 2016 7th EAI International Conference on Sensor Systems and Software » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung As 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. Maël Gay, Jan Burchard, Jan Horáček, Ange-Salomé Messeng Ekossono, Tobias Schubert, Bernd Becker, Ilia Polian, Martin KreuzerSmall Scale AES Toolbox: Algebraic and Propositional
Formulas, Circuit-Implementations and Fault Equations 2016 FCTRU'16 nach oben zur Jahresübersicht Jan Burchard, Tobias Schubert, Bernd BeckerLaissez-Faire Caching for Parallel #SAT Solving 2015 International Conference on Theory and Applications of Satisfiability Testing , Band : 9340, Seiten : 46 - 61» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung The problem of counting the number of satisfying assignments
of a propositional formula (#SAT) can be considered to be the big brother
of the well known SAT problem. However, the higher computational
complexity and a lack of fast solvers currently limit its usability for real
world problems.
Similar to SAT, utilizing the parallel computation power of modern
CPUs could greatly increase the solving speed in the realm of #SAT.
However, in comparison to SAT there is an additional obstacle for the
parallelization of #SAT that is caused by the usage of conflict learning
together with the #SAT specific techniques of component caching and
sub-formula decomposition. The combination can result in an incorrect
final result being computed due to incorrect values in the formula cache.
This problem is easily resolvable in a sequential solver with a depth-first
node order but requires additional care and handling in a parallel one. In
this paper we introduce laissez-faire caching which allows for an arbitrary
node computation order in both a sequential and parallel solver while
ensuring a correct final result. Additionally, we apply this new caching
approach to build countAntom, the world’s first parallel #SAT-solver.
Our experimental results clearly show that countAntom achieves con-
siderable speedups through the parallel computation while maintaining
correct results on a large variety of benchmarks coming from different
real-world applications. Moreover, our analysis indicates that laissez-faire
caching only adds a small computational overhead. Katrin Weber, Corinna Bertuzzi, Tobias SchubertKooperation 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 BeckerFormal 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» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Vulnerability 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. nach oben zur Jahresübersicht Sven Reimer, Matthias Sauer, Tobias Schubert, Bernd BeckerIncremental Encoding and Solving of Cardinality Constraints 2014 International Symposium on Automated Technology for Verification and Analysis , Springer International Publishing, Band : 8837, Seiten : 297 - 313» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Traditional 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 BeckerAccurate 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 BeckerExact 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» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Logic and fault simulation are essential tools in electronic design automation. The accuracy of standard
simulation algorithms is compromised by unknown or X-values. This results in a pessimistic overestimation
of X-valued signals in the circuit, and a pessimistic underestimation of fault coverage.
This work proposes efficient algorithms for combinational and sequential logic as well as for stuck-at and
transition-delay fault simulation which are free of any simulation pessimism in presence of unknowns. The
SAT-based algorithms exactly classifiy all signal states. During fault simulation, each fault is accurately
classified as either undetected, definitely detected or possibly detected.
The pessimism w. r. t. unknowns present in classic algorithms is thoroughly investigated in the experimental
results on benchmark circuits. The applicability of the proposed algorithms is demonstrated on
larger industrial circuits. The results show, that by accurate analysis the number of detected faults can be
significantly increased without increasing the test set size. Linus Feiten, Andreas Spilla, Matthias Sauer, Tobias Schubert, Bernd BeckerImplementation 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» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Ring 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 BeckerUsing MaxBMC for Pareto-Optimal Circuit Initialization
2014 Conf. on Design, Automation and Test in Europe » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In 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. nach oben zur Jahresübersicht Tobias Schubert, Jan Burchard, Matthias Sauer, Bernd BeckerS-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 BeckerAnalysis of Ring Oscillator PUFs on 60nm FPGAs 2013 TRUDEVICE Workshop, Avignon » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In hardware security and trusted computing it is often desired to uniquely and unambiguously identify a device among several others of the same brand. Physically unclonable functions (PUFs) take advantage of subtle variations in the devices' production process to achieve this. A ring oscillator (RO) PUF exploits differing time delays of circuits to yield a unique response from each device.
The 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 » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Vulnerability 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 SchaubAccurate Computation of Sensitizable Paths using Answer Set Programming 2013 Int. Conf. on Logic Programming and Nonmonotonic Reasoning , Seiten : 92 - 101» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Precise 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 BeckerApplying 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 » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present an approach to identify functional input sequences
in sequential circuits. The properties required are inserted as target of
a bounded model checking (BMC) problem, by using Craig interpolants
it can be stated whether sequences justifying the properties exist or
not. The initial state is either completely or partially unknown, and for
the latter we engage a MAX-SAT formulation to retrieve the shortest
sequence if a maximal subset of the initial state bits are unknown.
We apply this method to problems arising from digital circuit testing
domain, in which usually an arbitrary initial state is assumed, i.e., that
the circuit’s sequential elements (flip-flops) are assumed to be fully con-
trollable. However, since some of these states may be unreachable during
normal operation, this results in undesired secondary test conditions.
In this paper BMC is used to (1) test timing faults in a digital circuit,
thereby the test requirements are encoded as target properties. Our
method yields the shortest functional test-sequences that justify the target
properties or it proves that such a sequence does not exist. Furthermore,
(2) the initialization of circuits is considered. We analyze the length of
such sequences depending on the number of controllable flip-flops. Matthias Sauer, Sven Reimer, Tobias Schubert, Ilia Polian, Bernd BeckerEfficient SAT-Based Dynamic Compaction and Relaxation for Longest Sensitizable Paths 2013 Conf. on Design, Automation and Test in Europe , Seiten : 448 - 453» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Comprehensive 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 BeckerProvably Optimal Test Cube Generation Using Quantified Boolean Formula Solving 2013 ASP Design Automation Conf. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Circuits 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 BeckerSAT-based Analysis of Sensitisable Paths 2013 IEEE Design & Test of Computers , Band : 30, Nummer : 4, Seiten : 81 - 88» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung A 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 BeckerWaveform-Guided Fault Injection by Clock Manipulation 2013 TRUDEVICE Workshop 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» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In 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 SchaubAccurate 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 BeckerSAT-ATPG Using Preferences for Improved Detection of Complex Defect Mechanisms 2012 VLSI Test Symp. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Failures 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%. nach oben zur Jahresübersicht Stefan Kupferschmid, Matthew Lewis, Tobias Schubert, Bernd BeckerIncremental preprocessing methods for use in BMC 2011 Formal Methods in System Design , Band : 39, Seiten : 185 - 204» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Traditional incremental SAT solvers have achieved great success in the domain of Bounded Model Checking (BMC). Recently, modern solvers have introduced advanced preprocessing procedures that have allowed them to obtain high levels of performance. 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 GiunchigliaParallel QBF Solving with Advanced Knowledge Sharing 2011 Fundamenta Informaticae , Band : 107, Nummer : 2-3, Seiten : 139 - 166» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In 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 HerdeParallel SAT Solving in Bounded Model Checking 2011 Journal of Logic and Computation , Band : 21, Nummer : 1, Seiten : 5 - 21» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bounded 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 BeckerSAT-Based Analysis of Sensitisable Paths 2011 IEEE Design and Diagnostics of Electronic Circuits and Systems , Seiten : 93 - 98» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Manufacturing 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. nach oben zur Jahresübersicht Stefan Kupferschmid, Matthew Lewis, Tobias Schubert, Bernd BeckerIncremental Preprocessing Methods for use in BMC 2010 Int'l Workshop on Hardware Verification » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Traditional 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 BeckerExploiting 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» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In 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. nach oben zur Jahresübersicht Natalia Kalinnik, Tobias Schubert, Erika Ábrahám, Ralf Wimmer, Bernd BeckerPicoso - A Parallel Interval Constraint Solver 2009 Int'l Conf. on Parallel and Distributed Processing Techniques and Applications , CSREA Press, Seiten : 473 - 479» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This 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 BeckerComparison of Knowledge Sharing Strategies in a Parallel QBF Solver 2009 High-Performance Computing and Simulation Conference , Seiten : 161 - 167 Matthew Lewis, Tobias Schubert, Bernd BeckerDPLL-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 GiunchigliaEvaluation 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 BeckerPaMiraXT: 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 GiunchigliaPaQuBE: 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 BeckerQMiraXT - A Multithreaded QBF Solver 2009 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” nach oben zur Jahresübersicht Matthew Lewis, Tobias Schubert, Bernd BeckerMultithreaded SAT Solving 2007 ASP Design Automation Conf. , Seiten : 926 - 921 Martin Fränzle, Christian Herde, Tino Teige, S. Ratschan, Tobias SchubertEfficient 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 nach oben zur Jahresübersicht Martin Fränzle, Christian Herde, S. Ratschan, Tobias Schubert, Tino TeigeInterval 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 HerdeParallel SAT-Solving in Bounded Model Checking 2006 Int'l Workshop on Parallel and Distributed Methods in Verification , Springer-Verlag, Band : 4346, Seiten : 301 - 315» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Bounded 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. nach oben zur Jahresübersicht Matthew Lewis, Tobias Schubert, Bernd BeckerSpeedup 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» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung This paper describes and compares features and techniques modern SAT solvers utilize to maximize performance. Here we focus on: Implication Queue Sorting (IQS) combined with Early Conflict Detection Based BCP (ECDB); and a modified decision heuristic based on the combination of Variable State Independent Decaying Sum (VSIDS), Berkmin, and Sieges Variable Move to Front (VMTF). These features were implemented and compared within the framework of the MIRA SAT solver. The efficient implementation and analysis of these features are presented and the speedup and robustness each feature provides is demonstrated. Finally, with everything enabled (ECDB with IQS and advanced decision heuristics), MIRA was able to consistently outperform zChaff and even Forklift on the benchmarks provided, solving 37 out of 111 industrial benchmarks compared to zChaffs 21 and Forklifts 28. Tobias Schubert, Bernd BeckerA Hardware Lab Anywhere at Any Time 2005 Journal of Systemics, Cybernetics, and Informatics: JSCI , Band : 2, Nummer : 6 Tobias Schubert, Bernd BeckerAccelerating Boolean SAT Engines Using Hyper-Threading Technology 2005 Asian Applied Computing Conf. Tobias Schubert, Bernd BeckerKnowledge Sharing in a Microcontroller based Parallel SAT Solver 2005 Int'l Conf. on Parallel and Distributed Processing Techniques and Applications Tobias Schubert, Bernd BeckerLemma Exchange in a Microcontroller based Parallel SAT Solver 2005 IEEE Int'l Symp. on VLSI Tobias Schubert, Bernd Becker, Matthew LewisPaMira - A Parallel SAT Solver with Knowledge Sharing 2005 Int'l Workshop on Microprocessor Test and Verification , IEEE Computer Society, Band : 00, Seiten : 29 - 36» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In 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. nach oben zur Jahresübersicht Matthew Lewis, Tobias Schubert, Bernd BeckerEarly Conflict Detection Based BCP for SAT Solving 2004 Int'l Conf. on Theory and Applications of Satisfiability Testing , Seiten : 29 - 36» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Abstract. 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 BeckerA Distributed SAT Solver for Microchip Microcontroller 2004 Workshop on Parallel Systems and Algorithms Matthew Lewis, Tobias Schubert, Bernd BeckerEarly Conflict Detection Based SAT Solving 2004 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” Tobias Schubert, Bernd BeckerPICHAFF2 - A Hierarchical Parallel SAT Solver 2004 Int'l Workshop on Microprocessor Test and Verification Tobias Schubert, Bernd BeckerParallel SAT Solving with Microcontrollers 2004 Asian Applied Computing Conf. nach oben zur Jahresübersicht Tobias Schubert, Bernd BeckerPICHAFF: A Distributed SAT Solver for Microcontrollers 2003 Euromicro Conf. Tobias Schubert, Bernd BeckerA Hardware Lab Anywhere At Anytime 2003 Int'l Conf. on Education and Information Systems: Technologies and Applications , Seiten : 130 - 135 Andreas Hett, Tobias SchubertA Hardware Lab in a Pocket 2003 World Conf. on E-Learning in Corporate, Government, Healthcare, and Higher Education Tobias Schubert, Andreas HettA Hardware Lab in a Pocket 2003 Int'l Conf. on Multimedia and Information and Communication Technologies in Education Tobias Schubert, Bernd BeckerDas Mobile Hardware-Praktikum 2003 European Conf. on Media in Higher Education nach oben zur Jahresübersicht Rolf Drechsler, Nicole Drechsler, Elke Mackensen, Tobias Schubert, Bernd BeckerDesign 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 BeckerSpecialized 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 BeckerSpecialized Hardware for Implementation of Evolutionary Algorithms 2000 Conf. on Genetic and Evolutionary Computation , Seite : 369