DIMACS: Series in Discrete Mathematics and Theoretical Computer Science 1991; 628 pp; hardcover Volume: 3 ISBN10: 0821865943 ISBN13: 9780821865941 List Price: US$129 Member Price: US$103.20 Order Code: DIMACS/3
 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 17 were copublished with the Association for Computer Machinery (ACM). Table of Contents  E. M. Clarke, Jr.  Temporal logic model checking: Two techniques for avoiding the state explosion problem
 H. Eveking  Automatic verification of extensions of hardware descriptions
 D. K. Probst and H. F. Li  Using partialorder semantics to avoid the state explosion problem in asynchronous systems
 A. Valmari  A stubborn attack on state explosion
 G. Berthelot, C. Johnen, and L. Petrucci  PAPETRI: Environment for the analysis of PETRI nets
 S. Graf and B. Steffen  Compositional minimization of finite state systems
 O. Coudert, J. C. Madre, and C. Berthet  Verifying temporal properties of sequential machines without building their state diagrams
 A. Bouajjani, J.C. Fernandez, and N. Halbwachs  Minimal model generation
 J. R. Burch  Verifying liveness properties by verifying safety properties
 M. Barbeau and G. V. Bochmann  Extension of the Karp and Miller procedure to LOTOS specifications
 R. E. Bryant and C.J. H. Seger  Formal verification of digital circuits using symbolic ternary system models
 M. B. Josephs and J. T. Udding  An algebra for delayinsensitive circuits
 H. WongToi and D. L. Dill  Synthesizing processes and schedulers from temporal specifications
 P. Loewenstein and D. L. Dill  Verification of multiprocessor cache protocol using simulation relations and higherorder logic
 C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis  Memory efficient algorithms for the verification of temporal properties
 H. Hiraishi, S. Meki, and K. Hamaguchi  Vectorized model checking for computation tree logic
 R. Janicki and M. Koutny  On some implementation of optimal simulations
 C. H. Golaszewski and R. P. Kurshan  Taskdriven supervisory control of discrete event systems
 E. Madelaine and D. Vergamini  Finiteness conditions and structural construction of automata for all process algebras
 C. Pixley  A computation theory and implementation of sequential hardware equivalence
 P. Godefroid  Using partial orders to improve automatic verification methods
 B. Josko  A context dependent equivalence relation between Kripke structures
 G. Shurek and O. Grumberg  The modular framework of computeraided verification
 D. A. Carrington and K. A. Robinson  Tool support for the refinement calculus
 W. Peng and S. Purushothaman  A unified approach to the deadlock detection problem in networks of communicating finite state machines
 M. Bickford and M. Srivas  A computeraided verification tool for finite state controller systems
 J. M. Morris and M. Howard  Program verification by symbolic execution of hyperfinite ideal machines
 R. Cleaveland  On automatically distinguishing inequivalent processes
 V. Roy and R. de Simone  Auto/Autograph
 H. Nakamura, Y. Kukimoto, M. Fujita, and H. Tanaka  A data path verifier for register transfer level using temporal logic language Tokio
 P. Camurati, M. Gilli, P. Prinetto, and M. S. Reorda  Model checking and graph theory in sequential ATPG
 J. C. Lloret, P. Azéma, and F. Vernadat  Compositional design and verification of communication protocols, using labelled PETRI nets
 U. Buy and R. Moll  Liveness analysis and the automatic generation of concurrent programs
 K. Hamaguchi, H. Hiraishi, and S. Yajima  Branching time regular temporal logic for model checking with linear time complexity
 L. Ness  Issues arising in the analysis of L.0
 M. Langevin  Automated RTL verification based on predicate calculus
 V. Yodaiken  The algebraic feedback product of automata. A state machine based model of concurrent systems
 H. Cho, G. Hachtel, S.W. Jeong, B. Plessier, E. Schwarz, and F. Somenzi  Results on the interface between formal verification and ATPG
