Formal Methods in Computer-Aided Design

Chapter 1 Abstraction by Symbolic Indexing Transformations

Chapter 2 Counter-Example Based Predicate Discovery in Predicate Abstraction

Chapter 3 Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis

Chapter 4 Simplifying Circuits for Formal Verification Using Parametric Representation

Chapter 5 Generalized Symbolic Trajectory Evaluation — Abstraction in Action

Chapter 6 Analysis of Symbolic SCC Hull Algorithms

Chapter 7 Sharp Disjunctive Decomposition for Language Emptiness Checking

Chapter 8 Relating Multi-step and Single-Step Microprocessor Correctness Statements

Chapter 9 Modeling and Verification of Out-of-Order Microprocessors in UCLID

Chapter 10 On Solving Presburger and Linear Arithmetic with SAT

Chapter 11 Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods

Chapter 12 Qubos: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers

Chapter 13 Exploiting Transition Locality in the Disk Based Murϕ Verifier

Chapter 14 Traversal Techniques for Concurrent Systems

Chapter 15 A Fixpoint Based Encoding for Bounded Model Checking

Chapter 16 Using Edge-Valued Decision Diagrams for Symbolic Generation of Shortest Paths

Chapter 17 Mechanical Verification of a Square Root Algorithm Using Taylor’s Theorem

Chapter 18 A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols

Chapter 19 Model Checking the Design of an Unrestricted, Stuck-at Fault Tolerant, Asynchronous Sequential Circuit Using SMV

Chapter 20 Functional Design Using Behavioural and Structural Components

Chapter 21 Compiling Hardware Descriptions with Relative Placement Information for Parametrised Libraries

Chapter 22 Input/Output Compatibility of Reactive Systems

Chapter 23 Smart Play-out of Behavioral Requirements