2025

 nach oben zur Jahresübersicht

• Lukas Mentel, Tobias Seufert, Karsten Scheibler, Christoph Scholl
  Dead-Code Detection with IC3 using SMT-LIBv2 Solvers
  2025 MBMV
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this case study we evaluate an SMT-based IC3 implementation which is designed for formally proving the absence of dead-code in embedded C code. Our IC3 implementation is able to use any off-the-shelf SMT-LIBv2 solver which allows solving under assumptions and supports QF_BVFP. We extend the basic IC3 generalization techniques by splitting theory variables into intervals enabling more fine grained reasoning. We compare different state-of-the-art SMT-LIBv2 solvers and evaluate how their performance is affected by optimizations of IC3, like target enlargement or stronger generalization of proof obligations, as well as a preprocessing technique known as constant elimination that has proven to be very effective in our application context. We further evaluate how IC3 with SMT-LIBv2 solvers and interval-based generalization competes in comparison to iSAT3+IC3 as a part of BTC EmbeddedPlatform® which we currently consider the strongest stand-alone engine in dead-code detection on floating-point dominated benchmarks.

2024

 nach oben zur Jahresübersicht

• Christoph Scholl, Tobias Seufert, Fabian Siegwolf
  Hierarchical Stochastic SAT and Quality Assessment of Logic Locking
  2024 SAT
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Motivated by the application of quality assessment of logic locking we introduce Hierarchical Stochastic SAT (HSSAT) which generalizes Stochastic SAT (SSAT). We look into the complexity of HSSAT and for solving HSSAT formulas we provide a prototype solver which computes exact evaluation results (i.e., without any approximation and without any imprecision caused by numerical rounding errors). Finally, we perform an intensive experimental evaluation of our HSSAT solver in the context of quality assessment of logic locking.

2023

 nach oben zur Jahresübersicht

• Tobias Seufert, Felix Winterer, Christoph Scholl, Karsten Scheibler, Tobias Paxian, Bernd Becker
  Everything You Always Wanted to Know About Generalization of Proof Obligations in PDR
  2023 IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Band: 42, Nummer: 4, Seiten: 1351 - 1364
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this article we revisit the topic of generalizing proof obligations in bit-level Property Directed Reachability (PDR). We provide a comprehensive study which (1) determines the complexity of the problem, (2) thoroughly analyzes limitations of existing methods, (3) introduces approaches to proof obligation generalization that have never been used in the context of PDR, (4) compares the strengths of different methods from a theoretical point of view, and (5) intensively evaluates the methods on various benchmarks from Hardware Model Checking as well as from AI Planning.
• Tobias Seufert
  On Safety Verification using PDR and Reverse PDR
  2023 Dissertation

2022

 nach oben zur Jahresübersicht

• Tobias Seufert, Christoph Scholl, Arun Chandrasekharan, Sven Reimer, Tobias Welp
  Making PROGRESS in Property Directed Reachability
  2022 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022)
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  With Proof-Guided Restriction Skipping (PROGRESS) we present a fully automatic and complete approach for Hardware Model Checking under restrictions. We use the PROGRESS approach in the context of PDR/IC3 [9, 18]. Our implementation of PDR/IC3 restricts input signals as well as state bits of a circuit to constants in order to quickly explore long execution paths of the design. We are able to identify spurious proofs of safety along the way and exploit information from these proofs to guide the relaxation of the restrictions. Hence, we greatly improve the capability of PDR to find counterexamples, especially with long error paths. In experiments with HWMCC benchmarks our approach is able to double the amount of detected deep counterexamples in comparison to Bounded Model Checking as well as in comparison to PDR.

2021

 nach oben zur Jahresübersicht

• Tobias Seufert, Felix Winterer, Christoph Scholl, Karsten Scheibler, Tobias Paxian, Bernd Becker
  Everything You Always Wanted to Know About Generalization of Proof Obligations in PDR
  CoRR, Band: 2105.09169, 2021
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this paper we revisit the topic of generalizing proof obligations in bit-level Property Directed Reachability (PDR). We provide a comprehensive study which (1) determines the complexity of the problem, (2) thoroughly analyzes limitations of existing methods, (3) introduces approaches to proof obligation generalization that have never been used in the context of PDR, (4) compares the strengths of different methods from a theoretical point of view, and (5) intensively evaluates the methods on various benchmarks from Hardware Model Checking as well as from AI Planning.
• Karsten Scheibler, Felix Winterer, Tobias Seufert, Tino Teige, Christoph Scholl, Bernd Becker
  ICP and IC3
  2021 DATE, IEEE
  » 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 MBMV
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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

 nach oben zur Jahresübersicht

• Tobias Seufert, Christoph Scholl
  fbPDR: In-depth Combination of Forward and Backward Analysis in Property Directed Reachability
  2019 Conference on Design, Automation and Test in Europe (DATE)
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We describe a thoroughly interweaved forward and backward version of PDR/IC3 called fbPDR. Motivated by the complementary strengths of PDR and Reverse PDR and by related work showing the benefits of collaboration between the two, fbPDR lifts the combination to a new level. We lay the theoretical foundations for sharing information represented by learned lemmas between PDR and Reverse PDR and demonstrate the effectiveness of our approach on benchmarks from the Hardware Model Checking Competition.
• Tobias Seufert, Christoph Scholl
  fbPDR: In-depth Combination of Forward and Backward Analysis in Property Directed Reachability (extended abstract)
  2019 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  and demonstrate the effectiveness of our approach on benchmarks from the Hardware Model Checking Competition.

2018

 nach oben zur Jahresübersicht

• Tobias Seufert, Christoph Scholl
  Combining PDR and Reverse PDR for Hardware Model Checking
  2018 Conference on Design, Automation and Test in Europe (DATE)
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  combined approach.

2017

 nach oben zur Jahresübersicht

• Tobias Seufert, Christoph Scholl
  Sequential Verification Using Reverse PDR
  2017 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In the last few years IC3 resp. PDR made a great stir as a SAT-based hardware verification approach without needing to unroll the transition relation as in Bounded Model Checking (BMC). Motivated by different strengths of forward and backward traversal observed in BDD based model checking, we consider Reverse PDR which starts its analysis with the initial states instead of the unsafe states as in original PDR. We show great benefits of Reverse PDR both by a theoretical and an experimental analysis. Finally, we profit from parallelism offered by modern multi-core processors and use a portfolio approach combining the advantages of Reverse and original PDR.