2021

 back to the year overview

• 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”
  » show abstract« hide abstract
  Abstract

  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)
  » show abstract« hide abstract
  Abstract

  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”
  » show abstract« hide abstract
  Abstract

  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.

2019

 back to the year overview

• Leonie Feldbusch, Felix Winterer, Johannes Gramsch, Linus Feiten, Bernd Becker
  Gamification in a Classroom Response System for Academic Teaching
  2019 11th International Conference on Computer Supported Education (CSEDU)
  » show abstract« hide abstract
  Abstract

  The classroom response system SMILE (SMartphones In LEctures) is regularly used in academic lectures. Among other features, it enables lecturers to start quizzes that can be answered anonymously by students on their smartphones. This aims at both activating the students and giving them feedback about their understanding of the current content of the lecture. But even though many students use SMILE in the beginning of a course, the number of active participants tends to decrease as the term progresses. This paper reports the results of a study looking at incorporating gamification into SMILE to increase the students’ motivation and involvement. Game elements such as scores, badges and a leaderboard have been integrated paired with a post-processing feature enabling students to repeat SMILE quizzes outside of the lectures. The evaluations show that the gamification approach increased the participation in SMILE quizzes significantly.

2018

 back to the year overview

• Felix Neubauer, Jan Burchard, Pascal Raiola, Jochen Rivoir, Bernd Becker, Matthias Sauer
  Efficient Generation of Parametric Test Conditions for AMS Chips with an Interval Constraint Solver
  2018 IEEE VLSI Test Symposium (VTS'18)
  » show abstract« hide abstract
  Abstract

  The characterization of analog-mixed signal (AMS) silicon requires a suitable pattern set able to exercise the parametric operational space to – among other tasks – validate the correct (specified) working behaviour of the device under test. As experience shows, most of the unexpected problems occur for very specific value combinations of a few test condition variables that were not expected to have an influence. Additionally, restrictions on the operational conditions have to be taken into account. We present a method to efficiently create a set of test conditions to cover such a constrained search space with a user-defined density. First, an initial test condition set is generated using quasirandom Sobol sequences. Secondly, we analyse the test conditions to identify and fill uncovered areas in the parameter space using the in-house interval constraint solver iSAT3. The applicability of the method is demonstrated by experimental results on a 19-dimensional search space using a realistic set of constraints.
• Felix Neubauer, Jan Burchard, Pascal Raiola, Jochen Rivoir, Bernd Becker, Matthias Sauer
  High-Coverage AMS Test Space Optimization by Efficient Parametric Test Condition Generation
  2018 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen”
  » show abstract« hide abstract
  Abstract

  The characterization of analog-mixed signal (AMS) silicon requires a suitable pattern set able to exercise the parametric operational space to – among other tasks – validate the correct (specified) working behaviour of the device under test. As experience shows, most of the unexpected problems occur for very specific value combinations of a few test condition variables that were not expected to have an influence. Additionally, restrictions on the operational conditions have to be taken into account. We present a method to efficiently create a set of test conditions to cover such a constrained search space with a user-defined density. First, an initial test condition set is generated using quasirandom Sobol sequences. Secondly, we analyse the test conditions to identify and fill uncovered areas in the parameter space using the in-house interval constraint solver iSAT3. The applicability of the method is demonstrated by experimental results on a 19-dimensional search space using a realistic set of constraints.

2017

 back to the year overview

• Jan Burchard, Felix Neubauer, Pascal Raiola, Dominik Erb, Bernd Becker
  Evaluating the Effectiveness of D-Chains in SAT based ATPG
  2017 IEEE Latin American Test Symposium (LATS'17)
  » show abstract« hide abstract
  Abstract

  With the ever increasing size of today’s Very-Large-Scale-Integration (VLSI) designs new approaches for test pattern generation become more and more popular. One of the best known methods is SAT-based automatic test pattern generation (ATPG) which, in contrast to classical structural ATPG, first generates a mathematical representation of the problem in form of a Boolean formula. A specialized solver evaluates this representation to determine the testability of faults and extracts a test pattern in case a satisfying assignment was found. In order to increase the solving speed introduced the concept of D-chains which add additional information to the mathematical model. In return, this forces the solver to only consider assignments that might lead to a valid test pattern and thus reduce the search space. With the advent of incremental solving new concepts like the backward D-chain or even more recently an indirect D-chain were introduced. However, none of the previous publications tried to analyze and evaluate which of these methods is the most beneficial. In this paper we present a thorough investigation of the different D-chain concepts to evaluate which is the best method for different problems. In addition, we propose a new indirect D-chain algorithm with two extensions. Our experimental results show that depending on the incorporated D-chain the runtime can be reduced tremendously.
• 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”
  » show abstract« hide abstract
  Abstract

  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.
• Pascal Raiola, Jan Burchard, Felix Neubauer, Dominik Erb, Bernd Becker
  Evaluating the Effectiveness of D-chains in SAT-based ATPG and Diagnostic TPG
  2017 J Electron Test, volume: 33, issue: 6, pages: 751 - 767
  » show abstract« hide abstract
  Abstract

  The ever increasing size and complexity of today’s Very-Large-Scale-Integration (VLSI) designs requires a thorough investigation of new approaches for the generation of test patterns for both test and diagnosis of faults. SAT-based automatic test pattern generation (ATPG) is one of the most popular methods, where, in contrast to classical structural ATPG methods, first a mathematical representation of the problem in form of a Boolean formula is generated, which is then evaluated by a specialized solver. If the considered fault is testable, the solver will return a satisfying assignment, from which a test pattern can be extracted; otherwise no such assignment can exist. In order to speed up test pattern generation, the concept of D-chains was introduced by several researchers. Thereby supplementary clauses are added to the Boolean formula, reducing the search space and guiding the solver toward the solution. In the past, different variants of D-chains have been developed, such as the backward D-chain or the indirect D-chain. In this work we perform a thorough analysis and evaluation of the D-chain variants for test pattern generation and also analyze the impact of different D-chain encodings on diagnostic test pattern generation. Our experimental results show that depending on the incorporated D-chain the runtime can be reduced tremendously.

2016

 back to the year overview

• 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
  » show abstract« hide abstract
  Abstract

  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, pages: 177 - 184
  » show abstract« hide abstract
  Abstract

  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.), volume: 10028, pages: 186 - 201
  » show abstract« hide abstract
  Abstract

  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, 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, volume: 116, 2016
  » show abstract« hide abstract
  Abstract

  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.