Computer Aided Verification: 3rd International Workshop, CAV ’91 Aalborg, Denmark, July 1–4, 1991 Proceedings

Colin Sterling (auth.), Kim G. Larsen, Arne Skou (eds.)3540551794, 9783540551799

This volume contains the proceedings of the third International Workshop on Computer Aided Verification, CAV ’91, held in Aalborg, Denmark, July 1-4, 1991. The objective of this series of workshops is to bring together researchers and practitioners interested in the development and use of methods, tools and theories for automatic verification of (finite) state systems. The workshop provides a unique opportunity for comparing the numerous verification methods and associated verification tools, and the extent to which they may be utilized in application design. The emphasis is not only on new research results but also on the application of existing results to real verification problems. The papers in the volume areorganized into sections on equivalence checking, model checking, applications, tools for process algebras, the state explosion problem, symbolic model checking, verification and transformation techniques, higher order logic, partial order approaches, hardware verification, timed specification and verification, and automata.

---

Table of contents :
Taming infinite state spaces….Pages 1-1
Silence is golden: Branching bisimilarity is decidable for context-free processes….Pages 2-12
Computing distinguishing formulas for branching bisimulation….Pages 13-23
Compositional checking of satisfaction….Pages 24-36
An action based framework for verifying logical and behavioural properties of concurrent systems….Pages 37-47
A linear-time model-checking algorithm for the alternation-free modal mu-calculus….Pages 48-58
Automatic temporal verification of buffer systems….Pages 59-69
Mechanically checked proofs of kernel specifications….Pages 70-82
A top down approach to the formal specification of SCI cache coherence….Pages 83-91
Integer programming in the analysis of concurrent systems….Pages 92-102
The lotos model of a fault protected system and its verification using a petri net based approach….Pages 103-113
Error diagnosis in finite communicating systems….Pages 114-124
Temporal precondition verification of design transformations….Pages 125-135
PAM: A process algebra manipulator….Pages 136-146
The Concurrency Workbench with priorities….Pages 147-157
A proof assistant for PSF….Pages 158-168
Avoiding state explosion by composition of minimal covering graphs….Pages 169-180
“On the fly” verification of behavioural equivalences and preorders….Pages 181-191
Bounded-memory algorithms for verification on-the-fly….Pages 192-202
Generating BDDs for symbolic model checking in CCS….Pages 203-213
Vectorized symbolic model checking of computation tree logic for sequential machine verification….Pages 214-224
Functional extension of symbolic model checking….Pages 225-232
An automated proof technique for finite-state machine equivalence….Pages 233-243
From data structure to process structure….Pages 244-254
Checking for language inclusion using simulation preorders….Pages 255-265
A semantic driven method to check the fineteness of CCS processes….Pages 266-276
Using the HOL prove assistant for proving the correctness of term rewriting rules reducing terms of sequential behavior….Pages 277-287
Mechanizing a proof by induction of process algebra specifications in higher order logic….Pages 288-298
A two-level formal verification methodology using HOL and COSMOS….Pages 299-309
Efficient algorithms for verification of equivalences for probabilistic processes….Pages 310-321
Partial-order model checking: A guide for the perplexed….Pages 322-331
Using partial orders for the efficient verification of deadlock freedom and safety properties….Pages 332-342
Complexity results for POMSET languages….Pages 343-353
Mechanically verifying safety and liveness properties of delay insensitive circuits….Pages 354-364
Automating most parts of hardware proofs in HOL….Pages 365-375
An overview and synthesis on timed process algebras….Pages 376-398
Minimum and maximum delay problems in realtime systems….Pages 399-409
Formal verification of speed-dependent asynchronous circuits using symbolic model checking of Branching Time Regular Temporal Logic….Pages 410-420
Verifying properties of HMS machine specifications of real-time systems….Pages 421-431
A linear time process algebra….Pages 432-442
Deciding properties of regular real timed processes….Pages 443-453
An algebra of Boolean processes….Pages 454-465
Comparing generic state machines….Pages 466-476
An automata theoretic approach to Temporal Logic….Pages 477-487