Professur für Betriebssysteme - Universität Freiburg

Name	Tobias Seufert
Adresse	Technische Fakultät Albert-Ludwigs-Universität Georges-Köhler-Allee 51 79110 Freiburg
Büro	Gebäude 51, Raum 02...032
Telefon	+49 (0) 761 203 8149
eMail	seufert@informatik.uni-freiburg.de
Website	http://www.informatik.uni-freiburg.de/~seufert

Tobias Seufert

2022

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)
KurzfassungWith 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.

Karsten Scheibler, Felix Winterer, Tobias Seufert, Tino Teige, Christoph Scholl, Bernd Becker
ICP and IC3
2021 DATE, IEEE
KurzfassungIf 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
Kurzfassungon 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.

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)
KurzfassungWe 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”
Kurzfassungand demonstrate the effectiveness of our approach on benchmarks from the Hardware Model Checking Competition.

Tobias Seufert, Christoph Scholl
Combining PDR and Reverse PDR for Hardware Model Checking
2018 Conference on Design, Automation and Test in Europe (DATE)
Kurzfassungcombined approach.

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”
KurzfassungIn 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.