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.
