Computer-Aided Verification: 2nd International Conference, CAV '90 New Brunswick, NJ, USA, June 18–21, 1990 Proceedings

Temporal logic model checking: Two techniques for avoiding the state explosion problem....Pages 1-1
Automatic verification of extensions of hardware descriptions....Pages 2-12
Papetri : Environment for the analysis of PETRI nets....Pages 13-22
Verifying temporal properties of sequential machines without building their state diagrams....Pages 23-32
Formal verification of digital circuits using symbolic ternary system models....Pages 33-43
Vectorized model checking for computation tree logic....Pages 44-53
Introduction to a computational theory and implementation of sequential hardware equivalence....Pages 54-64
Auto/autograph....Pages 65-75
A data path verifier for register transfer level using temporal logic language Tokio....Pages 76-85
The use of model checking in ATPG for sequential circuits....Pages 86-95
Compositional design and verification of communication protocols, using labelled petri nets....Pages 96-105
Issues arising in the analysis of L.0....Pages 106-115
Automated RTL verification based on predicate calculus....Pages 116-125
On using protean to verify ISO FTAM protocol....Pages 126-135
Quantitative temporal reasoning....Pages 136-145
Using partial-order semantics to avoid the state explosion problem in asynchronous systems....Pages 146-155
A stubborn attack on state explosion....Pages 156-165
Using optimal simulations to reduce reachability graphs....Pages 166-175
Using partial orders to improve automatic verification methods....Pages 176-185
Compositional minimization of finite state systems....Pages 186-196
Minimal model generation....Pages 197-203
A context dependent equivalence relation between kripke structures....Pages 204-213
The modular framework of computer-aided verification....Pages 214-223
Verifying liveness properties by verifying safety properties....Pages 224-232
Memory efficient algorithms for the verification of temporal properties....Pages 233-242
A unified approach to the deadlock detection problem in networks of communicating finite state machines....Pages 243-252
Branching time regular temporal logic for model checking with linear time complexity....Pages 253-262
The algebraic feedback product of automata....Pages 263-271
Synthesizing processes and schedulers from temporal specifications....Pages 272-281
Task-driven supervisory control of discrete event systems....Pages 282-291
A proof lattice-based technique for analyzing liveness of resource controllers....Pages 292-301
Verification of a multiprocessor cache protocol using simulation relations and higher-order logic (summary)....Pages 302-311
Computer assistance for program refinement....Pages 312-321
Program verification by symbolic execution of hyperfinite ideal machines....Pages 322-332
Extension of the Karp and miller procedure to lotos specifications....Pages 333-342
An algebra for delay-insensitive circuits....Pages 343-352
Finiteness conditions and structural construction of automata for all process algebras....Pages 353-363
On automatically explaining bisimulation inequivalence....Pages 364-372