2017

 nach oben zur Jahresübersicht

• Jan Burchard, Maël Gay, Ange-Salomé Messeng Ekossono, Jan Horáček, Bernd Becker, Tobias Schubert, Martin Kreuzer, Ilia Polian
  AutoFault: 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 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
• Jan Burchard, Ange-Salomé Messeng Ekossono, Jan Horáček, Maël Gay, Bernd Becker, Tobias Schubert, Martin Kreuzer, Ilia Polian
  Towards 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 Polian
  Towards Mixed Structural-Functional Models for Algebraic Fault Attacks on Ciphers
  2017 International Verification and Security Workshop (IVSW) 2017

2016

 nach oben zur Jahresübersicht

• 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
  » 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.
• Jan Burchard, Tobias Schubert, Bernd Becker
  Distributed 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 Becker
  PackSens: 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 Kreuzer
  Small Scale AES Toolbox: Algebraic and Propositional 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
  » 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.
• 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
  » 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.

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
  » 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 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
  » 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 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
  » 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 Becker
  Using 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.

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, 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 Schaub
  Accurate 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.
• Linus Feiten, Andreas Spilla, Matthias Sauer, Tobias Schubert, Bernd Becker
  Analysis 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.
• 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
  » 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 Becker
  Efficient 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 Becker
  Provably 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 Becker
  SAT-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 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
  » 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 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.
  » 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%.

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 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 Giunchiglia
  Parallel 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 Herde
  Parallel 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 Becker
  SAT-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.

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
  » 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 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
  » 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.

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
  » 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 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
  » 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.

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
  » 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 Siege’s 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 zChaff’s 21 and Forklift’s 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
  » 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.

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
  » 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 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