Computer Aided Verification: 6th International Conference, CAV ’94 Stanford, California, USA, June 21–23, 1994 Proceedings

Rajeev Alur, Limor Fix, Thomas A. Henzinger (auth.), David L. Dill (eds.)3540581790, 9783540581796

This volume contains the proceedings of the 6th Conference on Computer Aided Verification, held at Stanford University in June 1994. The in total 37 included papers were selected in a highly competetive reviewing process from 121 submissions; in total they document many of the most important advances achieved in CAV research and applications since the predecessor conference held in June 1993.
The volume is organized in sections on Real-Time Systems, CAV Theory, CAV Applications, Symbolic Verification, Hybrid Systems, Model Checking, Improving Efficiency, and Hardware Verification.

---

Table of contents :
A determinizable class of timed automata….Pages 1-13
Real-time system verification using P/T nets….Pages 14-26
Criteria for the simple path property in timed automata….Pages 27-40
Hierarchical representations of discrete functions, with application to model checking….Pages 41-54
Symbolic verification with periodic sets….Pages 55-67
Automatic verification of pipelined microprocessor control….Pages 68-80
Using abstractions for the verification of linear hybrid systems….Pages 81-94
Decidability of hybrid systems with rectangular differential inclusions….Pages 95-104
Suspension automata: A decidable class of hybrid automata….Pages 105-117
Verification of context-free timed systems using linear hybrid observers….Pages 118-131
On the random walk method for protocol testing….Pages 132-141
An automata-theoretic approach to branching-time model checking (Extended abstract)….Pages 142-155
Realizability and synthesis of reactive modules….Pages 156-168
Model checking of macro processes….Pages 169-181
Methodology and system for practical formal verification of reactive hardware….Pages 182-193
Modeling and verification of a real life protocol using symbolic model checking….Pages 194-206
Verification of a distributed cache memory by using abstractions….Pages 207-219
Beyond model checking….Pages 220-221
Models whose checks don’t explode….Pages 222-233
On the automatic computation of network invariants….Pages 234-246
Ground temporal logic: A logic for hardware verification….Pages 247-259
A hybrid model for reasoning about composed hardware systems….Pages 260-272
Composing symbolic trajectory evaluation results….Pages 273-285
The completeness of a hardware inference system….Pages 286-298
Efficient model checking by automated ordering of transition relation partitions….Pages 299-310
The verification problem for safe replaceability….Pages 311-323
Formula-dependent equivalence for compositional CTL model checking….Pages 324-337
An improved algorithm for the evaluation of fixpoint expressions….Pages 338-350
Incremental model checking in the modal mu-calculus….Pages 351-363
Performance improvement of state space exploration by regular & differential hashing functions….Pages 364-376
Combining partial order reductions with on-the-fly model-checking….Pages 377-390
Improving language containment using fairness graphs….Pages 391-403
A parallel algorithm for relational coarsest partition problems and its implementation….Pages 404-414
Another look at LTL model checking….Pages 415-427
The mobility workbench — A tool for the π -Calculus….Pages 428-440
Compositional semantics of Esterel and verification by compositional reductions….Pages 441-454
Model checking using adaptive state and data abstraction….Pages 455-467
Automatic verification of timed circuits….Pages 468-480