Hardcover ISBN:  9780821865941 
Product Code:  DIMACS/3 
List Price:  $144.00 
MAA Member Price:  $129.60 
AMS Member Price:  $115.20 
eBook ISBN:  9781470439613 
Product Code:  DIMACS/3.E 
List Price:  $136.00 
MAA Member Price:  $122.40 
AMS Member Price:  $108.80 
Hardcover ISBN:  9780821865941 
eBook: ISBN:  9781470439613 
Product Code:  DIMACS/3.B 
List Price:  $280.00 $212.00 
MAA Member Price:  $252.00 $190.80 
AMS Member Price:  $224.00 $169.60 
Hardcover ISBN:  9780821865941 
Product Code:  DIMACS/3 
List Price:  $144.00 
MAA Member Price:  $129.60 
AMS Member Price:  $115.20 
eBook ISBN:  9781470439613 
Product Code:  DIMACS/3.E 
List Price:  $136.00 
MAA Member Price:  $122.40 
AMS Member Price:  $108.80 
Hardcover ISBN:  9780821865941 
eBook ISBN:  9781470439613 
Product Code:  DIMACS/3.B 
List Price:  $280.00 $212.00 
MAA Member Price:  $252.00 $190.80 
AMS Member Price:  $224.00 $169.60 

Book DetailsDIMACS  Series in Discrete Mathematics and Theoretical Computer ScienceVolume: 3; 1991; 628 ppMSC: Primary 68
This volume, published jointly with the Association for Computing Machinery, contains the proceedings of the second workshop on ComputerAided Verification, held at DIMACS at Rutgers University in June 1990. The motivation for the workshop was to bring together researchers working on effective algorithms or methodologies for formal verification (as distinguished from, for example, attributes of logics or formal languages). The theoretical results leading to new or more powerful verification methods include advances in the use of binary decision diagrams, dense time, reductions based on partial order representations, and proofchecking in controller verification.
The general focus of this volume is on the problem of making formal verification feasible for 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 and to exercise that tool on realistic examples. This volume provides a look at the latest theoretical advances in this exciting and important area of research.
Copublished with the Center for Discrete Mathematics and Theoretical Computer Science beginning with Volume 8. Volumes 1–7 were copublished with the Association for Computer Machinery (ACM).

Table of Contents

Chapters

Temporal logic model checking: Two techniques for avoiding the state explosion problem

Automatic verification of extensions of hardware descriptions

Using partialorder 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 delayinsensitive circuits

Synthesizing processes and schedulers from temporal specifications

Verification of multiprocessor cache protocol using simulation relations and higherorder logic

Memory efficient algorithms for the verification of temporal properties

Vectorized model checking for computation tree logic

On some implementation of optimal simulations

Taskdriven 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 computeraided verification

Tool support for the refinement calculus

A unified approach to the deadlock detection problem in networks of communicating finite state machines

A computeraided verification tool for finite state controller systems

Program verification by symbolic execution of hyperfinite ideal machines

On automatically distinguishing inequivalent processes

Auto/Autograph

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


RequestsReview Copy – for publishers of book reviewsAccessibility – to request an alternate format of an AMS title
 Book Details
 Table of Contents
 Requests
This volume, published jointly with the Association for Computing Machinery, contains the proceedings of the second workshop on ComputerAided Verification, held at DIMACS at Rutgers University in June 1990. The motivation for the workshop was to bring together researchers working on effective algorithms or methodologies for formal verification (as distinguished from, for example, attributes of logics or formal languages). The theoretical results leading to new or more powerful verification methods include advances in the use of binary decision diagrams, dense time, reductions based on partial order representations, and proofchecking in controller verification.
The general focus of this volume is on the problem of making formal verification feasible for 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 and to exercise that tool on realistic examples. This volume provides a look at the latest theoretical advances in this exciting and important area of research.
Copublished with the Center for Discrete Mathematics and Theoretical Computer Science beginning with Volume 8. Volumes 1–7 were copublished with the Association for Computer Machinery (ACM).

Chapters

Temporal logic model checking: Two techniques for avoiding the state explosion problem

Automatic verification of extensions of hardware descriptions

Using partialorder 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 delayinsensitive circuits

Synthesizing processes and schedulers from temporal specifications

Verification of multiprocessor cache protocol using simulation relations and higherorder logic

Memory efficient algorithms for the verification of temporal properties

Vectorized model checking for computation tree logic

On some implementation of optimal simulations

Taskdriven 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 computeraided verification

Tool support for the refinement calculus

A unified approach to the deadlock detection problem in networks of communicating finite state machines

A computeraided verification tool for finite state controller systems

Program verification by symbolic execution of hyperfinite ideal machines

On automatically distinguishing inequivalent processes

Auto/Autograph

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