This book, published jointly with the Association for Computing Machinery, contains the proceedings of the second workshop on Computer-Aided Verification, held at DIMACS at Rutgers University in June 1990. The general focus of this volume is on the problem of making formal verification feasible for the various models of computation. Specific emphasis is on models associated with distributed programs, protocols, and digital circuits. The general test of algorithm feasibility is to embed it into a verification tool on realistic examples. This volume looks at the latest theoretical advances in this exciting and important area of research.

Temporal logic model checking: Two techniques for avoiding the state explosion problem
Automatic verification of extensions of hardware descriptions
Using partial-order semantics to avoid the state explosion problem in asynchronous systems
A stubborn attack on state explosion
PAPETRI: Environment for the analysis of PETRI nets
Compositional minimization of finite state systems
Verifying temporal properties of sequential machines without building their state diagrams
Minimal model generation
Verifying liveness properties by verifying safety properties
Extension of the Karp and Miller procedure to LOTOS specifications
Formal verification of digital circuits using symbolic ternary system models
An algebra for delay-insensitive circuits
Synthesizing processes and schedulers from temporal specifications
Verification of multiprocessor cache protocol using simulation relations and higher-order logic
Memory efficient algorithms for the verification of temporal properties
Vectorized model checking for computation tree logic
On some implementation of optimal simulations
Task-driven supervisory control of discrete event systems
Finiteness conditions and structural construction of automata for all process algebras
A computation theory and implementation of sequential hardware equivalence
Using partial orders to improve automatic verification methods
A context dependent equivalence relation between Kripke structures
The modular framework of computer-aided verification
Tool support for the refinement calculus
A unified approach to the deadlock detection problem in networks of communicating finite state machines
A computer-aided verification tool for finite state controller systems
Program verification by symbolic execution of hyperfinite ideal machines
On automatically distinguishing inequivalent processes
Auto/Autograph
Simone A data path verifier for register transfer level using temporal logic language Tokio
Model checking and graph theory in sequential ATPG
Compositional design and verification of communication protocols, using labelled PETRI nets
Liveness analysis and the automatic generation of concurrent programs
Branching time regular temporal logic for model checking with linear time complexity
Issues arising in the analysis of L.0
Automated RTL verification based on predicate calculus
The algebraic feedback product of automata. A state machine based model of concurrent systems
Results on the interface between formal verification and ATPG
Table of Contents provided by Publisher. All Rights Reserved.

Supplemental Materials

What is included with this book?

The New copy of this book will include any supplemental materials advertised. Please check the title of the book to determine if it should include any access cards, study guides, lab manuals, CDs, etc.

The Used, Rental and eBook copies of this book are not guaranteed to include any supplemental materials. Typically, only the book itself is included. This is true even if the title states it includes any access cards, study guides, lab manuals, CDs, etc.