AMS Bookstore LOGO amslogo
Return to List  Item: 1 of 1   
Computer-Aided Verification '90
Edited by: E. M. Clarke and R. P. Kurshan
A co-publication of the AMS, DIMACS, and Association for Computing Machinery.

DIMACS: Series in Discrete Mathematics and Theoretical Computer Science
1991; 628 pp; hardcover
Volume: 3
ISBN-10: 0-8218-6594-3
ISBN-13: 978-0-8218-6594-1
List Price: US$129
Member Price: US$103.20
Order Code: DIMACS/3
[Add Item]

Request Permissions

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.

Co-published with the Center for Discrete Mathematics and Theoretical Computer Science beginning with Volume 8. Volumes 1-7 were co-published 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 partial-order 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 delay-insensitive circuits
  • H. Wong-Toi 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 higher-order 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 -- Task-driven 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 computer-aided 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 computer-aided 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
Powered by MathJax
Return to List  Item: 1 of 1   

  AMS Home | Comments:
© Copyright 2014, American Mathematical Society
Privacy Statement

AMS Social

AMS and Social Media LinkedIn Facebook Podcasts Twitter YouTube RSS Feeds Blogs Wikipedia