Computer-aided Verification: (DIMACS: Series in Discrete Mathematics and Theoretical Computer Science)

This volume, 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 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 proof-checking 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.

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