Formal Methods in Computer Aided Design - Title page

Introduction

Preface (PDF)

pp. viii

Referees (PDF)

pp. xi

Formal Methods in Computer Aided Design - Cover (PDF)

pp. c1

Formal Methods in Computer Aided Design - TOC (PDF)

pp. v-vii

Formal Methods in Computer Aided Design - Copyright (PDF)

pp. iv

Organizing Committee (PDF)

pp. ix

Program Committee (PDF)

pp. x

SAT-Based Methods

Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC (Abstract)

pp. 3-12

PDF

Improved Design Debugging Using Maximum Satisfiability (Abstract)

pp. 13-19

PDF

Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence Verification (Abstract)

pp. 20-26

PDF

Boosting Verification by Automatic Tuning of Decision Procedures (Abstract)

pp. 27-34

PDF

High-Level System Analysis

Verifying Correctness of Transactional Memories (Abstract)

pp. 37-44

PDF

Algorithmic Analysis of Piecewise FIFO Systems (Abstract)

pp. 45-52

PDF

Transaction Based Modeling and Verification of Hardware Protocols (Abstract)

Xiaofang Chen

Steven M. German

Ganesh Gopalakrishnan

pp. 53-61

PDF

Automating Hazard Checking in Transaction-Level Microarchitecture Models (Abstract)

Yogesh Mahajan

Sharad Malik

pp. 62-65

PDF

Krishnamani Kalyanasundaram

Abstraction-Based Methods

Computing Predicate Abstractions by Integrating BDDs and SMT Solvers (Abstract)

Roberto Cavada

Alessandro Cimatti

Anders Franz?en

Marco Roveri

R.K. Shyamasundar

pp. 69-76

PDF

Induction in CEGAR for Detecting Counterexamples (Abstract)

pp. 77-84

PDF

Lifting Propositional Interpolants to the Word-Level (Abstract)

Daniel Kroening

Georg Weissenbacher

pp. 85-89

PDF

Software Analysis Methods

Global Optimization of Compositional Systems (Abstract)

pp. 93-100

PDF

Cross-Entropy Based Testing (Abstract)

pp. 101-108

PDF

Symbolic Trajectory Evaluation

Automatic Abstraction Refinement for Generalized Symbolic Trajectory Evaluation (Abstract)

Fei Xie

pp. 111-118

PDF

A Logic for GSTE (Abstract)

Edward Smith

pp. 119-126

PDF

Automatic Abstraction in Symbolic Trajectory Evaluation (Abstract)

pp. 127-135

PDF

Specification Theory

A Coverage Analysis for Safety Property Lists (Abstract)

Koen Claessen

pp. 139-145

PDF

What Triggers a Behavior? (Abstract)

Orna Kupferman

Yoad Lustig

pp. 146-153

PDF

Two-Dimensional Regular Expressions for Compositional Bus Protocols (Abstract)

Kathi Fisler

pp. 154-157

PDF

A Quantitative Completeness Analysis for Property-Sets (Abstract)

pp. 158-161

PDF

Industrial-Strength Verification

Automated Extraction of Inductive Invariants to Aid Model Checking (Abstract)

pp. 165-172

PDF

Checking Safety by Inductive Generalization of Counterexamples to Induction (Abstract)

Aaron R. Bradley

Zohar Manna

pp. 173-180

PDF

Fast Minimum-Register Retiming via Binary Maximum-Flow (Abstract)

pp. 181-187

PDF

Formal Verification of Partial Good Self-Test Fencing Structures (Abstract)

pp. 188-191

PDF

Case study: Integrating FV and DV in the Verification of the Intel? Core^{TM} 2 Duo Microprocessor (Abstract)

pp. 192-195

PDF

Reasoning about Physical Systems

Circuit Level Verification of a High-Speed Toggle (Abstract)

Chao Yan

Mark R. Greenstreet

pp. 199-206

PDF

Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs (Abstract)

pp. 207-215

PDF

Analyzing Gene Relationships for Down Syndrome with Labeled Transition Graphs (Abstract)

pp. 216-219

PDF

Advanced Theorem-Proving Applications

A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware (Abstract)

Julien Schmaltz

pp. 223-230

PDF

Modeling Time-Triggered Protocols and Verifying Their Real-Time Schedules (Abstract)

Lee Pike

pp. 231-238

PDF

A Mechanized Refinement Framework for Analysis of Custom Memories (Abstract)

Sandip Ray

Jayanta Bhadra

pp. 239-242

PDF

Author Index

Author Index (PDF)

pp. 243-244