SAT-based verification - from core algorithms to novel application domains ; SAT-basierte Verifikation - von Basis-Algorithmen zu neuen Anwendungsdomänen
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Doctoral Thesis;
Electronic Thesis;
E-Book
Title:
SAT-based verification - from core algorithms to novel application domains ; SAT-basierte Verifikation - von Basis-Algorithmen zu neuen Anwendungsdomänen
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
In this thesis we discuss the verification of systems to guarantee their correct behavior, that is given by a specification, using formal techniques. For the work at hand, the mathematical and algorithmic methods that are used for this verification task are the application of the so-called model checking technique that is combined with automated proof systems for solving the satisfiability problem (short: SAT). SAT-based verification of circuits and discrete systems has become one of the most effective technique within the last 10 years, such that industrial as well as academic applications heavily rely on it. SAT-based verification is the topic of this thesis, too, whereby our contributions cover the whole range of a SAT-based tool application. This means in practical terms that we propose extensions and concepts that concentrate on the core of a SAT-solver. However, these proposals are then transfered to novel verification models such as linear hybrid automata. Furthermore, we describe and evaluate approaches that incorporate the structure of the underlying problem to exploit knowledge gained during the verification process on the level of the SAT-solver. The main focus of the thesis at hand is on the verification of incomplete system designs, which occur for example in the early phase of a design. Our contributions are several SAT-based modeling techniques for the verification of such incomplete system designs. We describe various modeling concepts that can be embedded into a taxonomy with respect to their expressiveness and required computational resources, such that depending on the complexity of the underlying verification problem different methods are available, thus assuring a flexible approach for the desired verification. The proposed methods are evaluated experimentally to guarantee their applicability in practice. Taken together, this thesis provides contributions to the state-of-the-art in SAT-based verification, starting from core algorithms up to novel application domains. ; In dieser Arbeit geht ...