2021

 nach oben zur Jahresübersicht

• Lukas Mentel, Karsten Scheibler, Felix Winterer, Bernd Becker, Tino Teige
  Benchmarking SMT Solvers on Automotive Code
  2021 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Using embedded systems in safety-critical environments requires a rigorous testing of the components these systems are composed of. For example, the software running on such a system has to be evaluated regarding its code coverage – in particular, unreachable code fragments have to be avoided according to the ISO 26262 standard. Software model checking allows to detect such dead code automatically. While the recent case study compares several academic software model checkers with the commercial test and verification tool BTC EmbeddedPlatform (BTC EP), we want to focus on a lower level – i.e. the back-end solvers within BTC EP. Therefore, we evaluate the performance of off-the-shelf SMT solvers supporting the theory of floating-point as well as the theory of bitvectors on floating-point dominated benchmark instances originating from the automotive domain. Furthermore, we compare these off-the-shelf SMT solvers with the back-end solvers used by BTC EP.
• Karsten Scheibler, Felix Winterer, Tobias Seufert, Tino Teige, Christoph Scholl, Bernd Becker
  ICP and IC3
  2021 Conference on Design, Automation and Test in Europe Conference (DATE)
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  If embedded systems are used in safety-critical environments, they need to meet several standards. For example, in the automotive domain the ISO 26262 standard requires that the software running on such systems does not contain unreachable code. Software model checking is one effective approach to automatically detect such dead code. Being used in a commercial product, iSAT3 already performs very well in this context. In this paper we integrate IC3 into iSAT3 in order to improve its dead code detection capabilities even further.
• Felix Winterer, Tobias Seufert, Karsten Scheibler, Tino Teige, Christoph Scholl, Bernd Becker
  ICP and IC3 with Stronger Generalization
  2021 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Most recently, IC3 was integrated into the SMT solver iSAT3. Thus, iSAT3+IC3 introduces the first IC3 variant based on interval abstraction and Interval Constraint Propagation (ICP). As strong generalization is one of the key aspects for the IC3 algorithm to be successful, we integrate two additional generalization schemes from literature into iSAT3+IC3: Inductive Generalization and Counterexamples To Generalization (CTG). Furthermore, we evaluate the benefits and the drawbacks of different variants of these methods in the context of interval abstraction and ICP.

2018

 nach oben zur Jahresübersicht

• Linus Feiten, Karsten Scheibler, Bernd Becker, Matthias Sauer
  Using different LUT paths to increase area efficiency of RO-PUFs on Altera FPGAs
  2018 TRUDEVICE Workshop, Dresden
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Furthermore, the number of PUF response bits can be increased even further without extra hardware or software if a certain degree of correlations among the response bits is accepted. The degree of correlations is proportional to the growth of response bits, so a design decision can be made. To make this decision, a metric to quantify the degree of correlations is needed, which has so far been mostly neglected in the analyses of PUF implementations.

2017

 nach oben zur Jahresübersicht

• Felix Neubauer, Karsten Scheibler, Bernd Becker, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer
  Accurate Dead Code Detection in Embedded C Code by Arithmetic Constraint Solving (Extended Abstract)
  2017 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Unreachable code fragments in software, despite not having a negative impact on the functional behavior, can have a bad effect in other areas, such as code optimization or coverage-based code validation and certification. Especially the latter is important in industrial, safety critical environments, where detecting such dead code is a major goal to adjust the coverage of software tests. In the context of embedded systems we focus on C programs which are reactive, control-oriented, and floating-point dominated. Such programs are either automatically generated from Simulink-plus-Stateflow models or hand-written according to coding guidelines. While there are various techniques – e.g. abstract interpretation or Counterexample guided abstraction refinement (CEGAR) – to deal with individual issues of this domain, there is none which can cover all of them. The AVACS transfer project T1 aims at the combination of these techniques in order to provide an accurate and efficient dead code detection. In this paper we present the ideas and goals of the project as well as the current status (including very promising experimental results) and future challenges.
• Universität Freiburg / FreiDok
  Applying CDCL to Verification and Test: When Laziness Pays Off
  
  Karsten Scheibler
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  When condensing this thesis into three keywords then CDCL, lazy and iSAT3 are the most important ones. The term CDCL is the abbreviation for conflict-driven clause learning and is the current state-of-the-art algorithm when searching for solutions for a given Boolean formula. For the moment the most important aspect is that CDCL does its job by operating on a set of so-called clauses. While some of the aforementioned problems can be expressed with a small set of these clauses which fits into the memory of currently available computers, other problems do not allow such an encoding. This is the point at which the term lazy comes into play. Instead of trying to generate all clauses in advance, some form of clever laziness is applied and the creation of a clause is deferred until it is really needed. This allows to tackle more complex problems which could not be solved before. In particular the solver iSAT3 relies on this technique for solving formulas with Boolean, integer, floating-point and real-valued variables. This solver is the basis of all contributions presented in this thesis.

2016

 nach oben zur Jahresübersicht

• Matthias Sauer, Sven Reimer, Daniel Tille, Karsten Scheibler, Dominik Erb, Ulrike Pfannkuchen, Bernd Becker
  Clock Cycle Aware Encoding for SAT-based Circuit Initialization
  2016 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen”
• Felix Neubauer, Karsten Scheibler, Bernd Becker, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer
  Accurate Dead Code Detection in Embedded C Code by Arithmetic Constraint Solving
  2016 First International Workshop on Satisfiability Checking and Symbolic Computation - FETOPEN-CSA SC2 Workshop - Affiliated with SYNASC 2016
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Unreachable code fragments in software, despite not having a negative impact on the functional behavior, can have a bad effect in other areas, such as code optimization or coverage-based code validation and certification. Especially the latter is important in industrial, safety critical environments, where detecting such dead code is a major goal to adjust the coverage of software tests. In the context of embedded systems we focus on C programs which are reactive, control-oriented, and floating-point dominated. Such programs are either automatically generated from Simulink-plus-Stateflow models or hand-written according to coding guidelines. While there are various techniques – e.g. abstract interpretation or Counterexample guided abstraction refinement (CEGAR) – to deal with individual issues of this domain, there is none which can cover all of them. The AVACS transfer project T1 aims at the combination of these techniques in order to provide an accurate and efficient dead code detection. In this paper we present the ideas and goals of the project as well as the current status (including very promising experimental results) and future challenges.
• Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer, Bernd Becker
  Accurate ICP-based Floating-Point Reasoning
  2016 Formal Methods in Computer-Aided Design, Seiten: 177 - 184
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In scientific and technical software, floating-point arithmetic is often used to approximate arithmetic on physical quantities natively modeled as reals. Checking properties for such programs (e.g. proving unreachability of code fragments) requires accurate reasoning over floating-point arithmetic. Currently, most of the SMT-solvers addressing this problem class rely on bit-blasting. Recently, methods based on reasoning in interval lattices have been lifted from the reals (where they traditionally have been successful) to the floating-point numbers. The approach presented in this paper follows the latter line of interval-based reasoning, but extends it by including bitwise integer operations and cast operations between integer and floating-point arithmetic. Such operations have hitherto been omitted, as they tend to define sets not concisely representable in interval lattices, and were consequently considered the domain of bit-blasting approaches. By adding them to interval-based reasoning, the full range of basic data types and operations of C programs is supported. Furthermore, we propose techniques in order to mitigate the problem of aliasing during interval reasoning. The experimental results confirm the efficacy of the proposed techniques. Our approach outperforms solvers relying on bit-blasting as well as the existing interval-based SMT-solver.
• Ahmed Mahdi, Karsten Scheibler, Felix Neubauer, Martin Fränzle, Bernd Becker
  Advancing software model checking beyond linear arithmetic theories
  2016 12th International Haifa Verification Conference, HVC 2016, Haifa, Israel, November 14-17, 2016 Twelfth Haifa Verification Conference 2016, Bloem, Roderick, Arbel, Eli (Eds.), Band: 10028, Seiten: 186 - 201
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Motivated by the practical need for verifying embedded control programs involving linear, polynomial, and transcendental arithmetics, we demonstrate in this paper a CEGAR technique addressing reachability checking over that rich fragment of arithmetics. In contrast to previous approaches, it is neither based on bit-blasting of floating-point implementations nor confined to decidable fragments of real arithmetic, namely linear or polynomial arithmetic. Its CEGAR loop is based on Craig interpolation within the iSAT3 SMT solver, which employs (abstract) conflict-driven clause learning (CDCL) over interval domains together with interval constraint propagation. As usual, the interpolants thus obtained on spurious counterexamples are used to subsequently refine the abstraction, yet in contrast to manipulating and refining the state set of a discrete-state abstraction, we propose a novel technique for refining the abstraction, where we annotate the abstract model’s transitions with side-conditions summarizing their effect. We exploit this for implementing case-based reasoning based on assumption-commitment predicates extracted from the stepwise interpolants in a lazy abstraction mechanism. We implemented our approach within iSAT3 and demonstrate its effectiveness by verifying several benchmarks.
• Karsten Scheibler, Dominik Erb, Bernd Becker
  Applying Tailored Formal Methods to X-ATPG
  2016 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  However, usually, one can not assume full control of all sequential elements and primary inputs. Therefore, uninitialized flip-flops may occur in the design -- leading to binary but unknown values (X-values). Classically, these X-values are handled by three-valued logic (01X). But this introduces pessimism when X-values reconverge in the circuit. On the other hand, the expressiveness of QBF allows to encode the unknown values accurately -- but comes at the cost of much higher runtimes. Therefore, we presented in [1] an accurate SAT-based CEGAR approach for automatic test pattern generation (ATPG) in presence of X-values. This approach is tailored to and optimized for this specific problem class and could also be used for closely related topics such as equivalence checking in presence of X-values. Although the approach is similar to an existing CEGAR-based 2-QBF solving algorithm, we show that our method has up to 50x lower runtimes. This underlines that an efficient CNF-encoding of a problem together with the fastest available standard solver does not guarantee optimal performance. Tailoring the underlying formal methods to the target problem class may give remarkable speedups on top.
• Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer, Bernd Becker
  Extending iSAT3 with ICP-Contractors for Bitwise Integer Operations
  AVACS Technical Report, SFB/TR 14 AVACS, Subproject T1, Band: 116, 2016
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Up to now SMT-solvers addressing floating-point arithmetic were based on bit-blasting. Quite recently, methods based on interval constraint propagation (ICP) for accurate reasoning over floating-point arithmetic were proposed. One prominent use-case for such methods is automatic dead-code detection in floating-point dominated embedded C programs. However, C programs usually contain a mix of floating-point arithmetic, integer arithmetic and bitwise integer operations. Thus, adding ICP-based support for floating-point arithmetic is not enough – bitwise integer operations have to be supported as well. Therefore, this report gives a detailed overview how these operations can be handled with ICP.
• Dominik Erb, Karsten Scheibler, Michael A. Kochte, Matthias Sauer, Hans-Joachim Wunderlich, Bernd Becker
  Mixed 01X-RSL-Encoding for Fast and Accurate ATPG with Unknowns
  2016 21st Asia and South Pacific Design Automation Conference
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this paper, we propose new ATPG techniques to overcome such limitations. An efficient hybrid encoding combines the accuracy of RSL-based modeling with the compactness of conventional three-valued encoding. A low-cost two-valued SAT-based untestability check is able to classify most untestable faults with low runtime. An incremental and event-based accurate fault simulator is introduced to reduce fault simulation effort. The experiments demonstrate the effectiveness of the proposed techniques. On average, over 99.3% of the faults are accurately classified. Both the number of aborts and the total runtime are significantly reduced compared to the state-of-the-art pure RSL-based algorithm. For circuits up to a million gates, the fault coverage could be increased considerably compared to a state-of-the-art commercial tool with very competitive runtimes.
• Karsten Scheibler, Dominik Erb, Bernd Becker
  signs
  2016 Conf. on Design, Automation and Test in Europe
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Therefore, this paper focuses on a new highly incremental CEGAR-based algorithm that overcomes these limitations and hence is completely accurate in presence of unknown values. It relies on a modified SAT-solver tailored to this specific problem. The experimental results for circuits with up to 2.400.000 gates show that this combination allows high accuracy and high scalability at the same time. Compared to a state-of-the-art commercial tool, the fault coverage could be increased significantly. Furthermore, the runtime is reduced remarkably compared to a QBF-based encoding of the problem.

2015

 nach oben zur Jahresübersicht

• Karsten Scheibler, Dominik Erb, Bernd Becker
  Improving Test Pattern Generation in Presence of Unknown Values beyond Restricted Symbolic Logic
  2015 to be published at European Test Symposium (ETS)
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this paper, we improve test generation based on RSL in two directions in order to reduce the gap to QBF further. First, we present techniques to go beyond the accuracy of RSL when generating test patterns. Second, we include a check which is able to accurately identify untestable faults. Experimental results show the high efficiency of the proposed method classifying almost all faults as testable or proving untestability.
• Dominik Erb, Karsten Scheibler, Matthias Sauer, Sudhakar M. Reddy, Bernd Becker
  Multi-Cycle Circuit Parameter Independent ATPG for Interconnect Open Defects
  2015 33rd VLSI Test Symposium (VTS)
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this work we extend the validity of CPI tests by introducing so-called multi-cycle CPI tests and single-value CPI tests. By doing so, we significantly improve the coverage of open defects and ensure their detection whilst including the additional effect of leakage currents on opens. Experimental results for circuits with over 500k non-equivalent faults and several thousand aggressors %deriving the new classes of CPI tests show the effectiveness of the newly proposed CPI tests as well as the high efficiency of a new ATPG algorithm to generate these new classes of CPI tests.
• Karsten Scheibler, Leonore Winterer, Ralf Wimmer, Bernd Becker
  Towards Verification of Artificial Neural Networks
  2015 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this paper we take a typical control problem, namely the Cart Pole System (a.k.a. inverted pendulum), and a model of its physical environment and study safety verification of this system. To do so, we use bounded model checking (BMC). The created formulas are solved with the SMT-solver iSAT3. We examine the problems that occur during solving these formulas and show that extending the solver by special deduction routines can reduce both memory consumption and computation time on such instances significantly. This constitutes a first step towards verification of machine-learned controllers, but a lot of challenges remain.

2014

 nach oben zur Jahresübersicht

• Dominik Erb, Karsten Scheibler, Matthias Sauer, Sudhakar M. Reddy, Bernd Becker
  for Interconnect Open Defects
  2014 23nd IEEE Asian Test Symposium (ATS)
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  faults and several thousand aggressors.
• Dominik Erb, Karsten Scheibler, Michael Kochte, Matthias Sauer, Hans-Joachim Wunderlich, Bernd Becker
  Based on Restricted Symbolic Logic
  2014 Int'l Test Conf.
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  more scalable and more robust.
• Dominik Erb, Karsten Scheibler, Matthias Sauer, Bernd Becker
  Efficient SMT-based ATPG for Interconnect Open Defects
  2014 Conf. on Design, Automation and Test in Europe
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  magnitude.
• Karsten Scheibler, Bernd Becker
  Implication Graph Compression inside the SMT Solver iSAT3
  2014 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  nations of linear and non-linear arithmetic constraint formulas (including transcendental functions), and thus is suitable to verify safety properties of systems consisting of both, linear and non-linear behaviour. The iSAT algorithm tightly integrates interval constraint propagation into the conflict-driven clause-learning framework. During the solving process, this may result in a huge implication graph. This paper presents a method to compress the implication graph on-the-fly. Experiments demonstrate that this method is able to reduce the overall memory footprint up to an order of magnitude.
• Karsten Scheibler, Bernd Becker
  Using Interval Constraint Propagation for Pseudo-Boolean Constraint Solving
  2014 Formal Methods in Computer-Aided Design
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Derived from the SMT solver iSAT3 we present the solver iSAT3p that on the one hand allows the efficient handling of huge pseudo-Boolean constraints with several thousand summands and large integer coefficients. On the other hand, experimental results demonstrate that at the same time iSAT3p is competitive or even superior to other solvers on standard pseudo-Boolean benchmark families.

2013

 nach oben zur Jahresübersicht

• Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd Becker
  A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
  2013 CADE, Springer, Band: 7898, Seiten: 193 - 207
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  A symbiosis of iSAT and CAD combines the advantages of both methods resulting in a fast and complete solver. In particular, the interval box determined by iSAT provides precious extra information to guide the CAD-method search routine: We use the interval box to prune the CAD search space in both phases, the projection and the construction phase, forming a search `tube' rather than a search tree. This proves to be particularly beneficial for a CAD implementation designed to search a satisfying assignment pointedly, as opposed to search and exclude conflicting regions.
• Karsten Scheibler, Matthias Sauer, Kohei Miyase, Bernd Becker
  Controlling Small-Delay Test Power Consumption using Satisfibility Modulo Theory Solving
  2013 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  monstrate the applicability of the method.
• Karsten Scheibler, Stefan Kupferschmid, Bernd Becker
  Recent Improvements in the SMT Solver iSAT
  2013 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Over the past decades embedded systems have become more and more complex. Furthermore, besides digital components they now often contain additional analog parts -- making them to embedded hybrid systems. If such systems are used in safety critical environments, a formal correctness proof is highly desirable. The SMT solver iSAT aims at solving boolean combinations of linear and non-linear constraint formulas (including transcendental functions), and thus is suitable to verify safety properties of systems consisting of both, linear and non-linear behaviour. To keep up with the ever increasing complexity of these systems we present recent improvements in various parts of iSAT. Experiments demonstrate that iSAT with all the presented improvements integrated typically gains a speedup between one and two orders of magnitude.

2011

 nach oben zur Jahresübersicht

• Andreas Eggers, Evgeny Kruglov, Stefan Kupferschmid, Karsten Scheibler, Tino Teige, Christoph Weidenbach
  Superposition modulo non-linear arithmetic
  2011 Int'l Symp. on Frontiers of Combining Systems, Springer, Seiten: 119 - 134
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  The first-order theory over non-linear arithmetic including transcendental functions (NLA) is undecidable.Nevertheless, in this paper we show that a particular combination with superposition leads to a sound and complete calculus that is useful in practice. We follow basically the ideas of the SUP(LA) combination, but have to take care of undecidability, resulting in ``unknown'' answers by the NLA reasoning procedure. A pipeline of NLA constraint simplification techniques related to the SUP(NLA) framework significantly decreases the number of ``unknown'' answers.The resulting approach is implemented as SUP(NLA) by a system combination of SPASS\ and iSAT. Applied to various scenarios of traffic collision avoidance protocols, we show by experiments that SPASS(iSAT) can fully automatically proof and disproof safety properties of such protocols using the very same formalization.