Global ETD Search
Search theses and dissertations gathered from participating repositories worldwide. Every result links back to the library that holds it. No account is needed.
Results
Showing 1 to 13 of 13 for “"Bounded Model Checking"”.
-
SMT-based bounded model checking of multi-threaded software in embedded systems
… effectively about large embedded software using bounded model checking (BMC) based on Satisfiability Modulo Theories (SMT) techniques. We present three major novel contributions. First, we extend the encodings from previous SMT-based bounded model checkers to provide more accurate support for …
-
Reachability Analysis of RTL Circuits Using k-Induction Bounded Model Checking and Test Vector Compaction
… of this thesis, a novel approach for k-induction bounded model checking using signal domain constraints and property partitioning for proving unreachability of branches in Verilog RTL code is presented. To do this, it approach uses program slicing with respect to the variables of the property …
-
Design Verification for Sequential Systems at Various Abstraction Levels
… performance and capacity of a typical SAT-based bounded model checking framework. Secondly, we present a novel method for performing dynamic abstraction within a framework for abstraction-refinement based model checking. Experiments on a wide range of industrial designs have shown that the …
-
Strategies for SAT-Based Formal Verification
… that they can be proven faster and interleave bounded reachability analysis with bounded model checking. We provide the necessary algorithms and implementation details in order to automate the proposed techniques. Experiments conducted on a variety of benchmark circuits show that orders of …
-
Efficient Graph Techniques for Partial Scan Pattern Debug and Bounded Model Checkers
… Debugger for Partial Scan Designs • Circuit SAT Bounded Model Checkers We developed a complete Interactive Scan Pattern Debugger Suite currently being used in the industry for next generation microprocessor design. The back end is an implication graph based sequential logic simulator which …
-
Identification and Analysis of Illegal States in the Apoptotic Discrete Transition System Model using ATPG and SAT-based Techniques
… of Biological systems. Previously, an abstracted model has been developed to study the Apoptosis process as a Finite State Discrete Transition Model. This model facilitates the reutilization of the digital design verification and testing techniques developed in the Electronic Design Automation …
-
Constraint Solving for Diagnosing Concurrency Bugs
… of constraint satisfiability (SAT) solvers and a bounded model checker, we perform a semantic analysis of the sequential computation as well as the thread interactions. The analysis is ideally suited for handling software with small to medium code size but complex concurrency control, such as …
-
System verification tools based on Monadic Logics
In der Mitte des letzten Jahrhunderts erschienen die ersten Arbeiten über monadische Logiken zweiter Stufe. Das Interesse an diesen Logiken lag zunächst hauptsächlich an Entscheidbarkeitsfragen von arithmetischen Theorien. Die monadischen Logiken zweiter Stufe über Wörter und Bäume gehören zu den …
-
Exploring Abstraction Techniques for Scalable Bit-Precise Verification of Embedded Software
… more formal verification techniques have begun modeling a non-Boolean data variable as a bit-vector with bounded width (i.e. a vector of multiple bits like 32- or 64- bits) to implement bit-precise verification. One major challenge in the scalable application of such bit-precise verification on …
-
Towards Practical Predicate Analysis
Software model checking is a successful technique for automated program verification. Several of the most widely used approaches for software model checking are based on solving first-order-logic formulas over predicates using SMT solvers, e.g., predicate abstraction, bounded model checking, …
-
Strategies for Performance and Quality Improvement of Hardware Verification and Synthesis Algorithms
… various EDA applications such as equivalence checking, model checking, Automatic Test Pattern Generation (ATPG), functional Bi-decomposition, and technology mapping need to keep pace with these challenges. In this thesis, we are concerned with improving the quality and performance of different …
-
Enhancing SAT-based Formal Verification Methods using Global Learning
… methods for design verification are Equivalence Checking and Model Checking. Equivalence Checking requires that the implementation circuit should be exactly equivalent to the specification circuit (golden model). In other words, for each possible input pattern, the implementation circuit should …
-
On Reducing the Trusted Computing Base in Binary Verification
The translation of binary code to higher-level models has wide applications, including decompilation, binary analysis, and binary rewriting. This calls for high reliability of the underlying trusted computing base (TCB) of the translation methodology. A key challenge is to reduce the TCB by …