Computer Aided Verification: Fourth International Workshop, CAV ’92 Montreal, Canada, June 29 – July 1, 1992 Proceedings

Leslie Lamport (auth.), Gregor von Bochmann, David Karl Probst (eds.)3540564969, 9783540564966

This volume gives the proceedings of the Fourth Workshop on Computer-Aided Verification (CAV ’92), held in Montreal, June 29 – July 1, 1992. 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 the computer-aided verification of concurrent systems. The workshops provide an opportunity for comparing various verification methods and practical tools that can be used to assist the applications designer. Emphasis is placed on new research results and the application of existing results to real verification problems. The volume contains 31 papers selected from 75 submissions. These are organized into parts on reduction techniques, proof checking, symbolic verification, timing verification, partial-order approaches, case studies, model and proof checking, and other approaches. The volume starts with an invited lecture by Leslie Lamport entitled “Computer-hindered verification (humans can do it too)”.

---

Table of contents :
Computer-hindered verification (humans can do it too)….Pages 1-1
Modular abstractions for verifying real-time distributed systems….Pages 2-15
Layering techniques for development of parallel systems….Pages 16-29
Efficient local correctness checking….Pages 30-43
Mechanical verification of concurrent systems with TLA….Pages 44-55
Using a theorem prover for reasoning about concurrent algorithms….Pages 56-68
Verifying a logic synthesis tool in Nuprl: A case study in software verification….Pages 69-81
Higher-level specification and verification with BDDs….Pages 82-95
Symbolic bisimulation minimisation….Pages 96-108
Towards a verification technique for large synchronous circuits….Pages 109-122
Verifying timed behavior automata with nonbinary delay constraints….Pages 123-136
Timing verification by successive approximation….Pages 137-150
A verification strategy for timing constrained systems….Pages 151-163
Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits….Pages 164-177
State space caching revisited….Pages 178-191
Verification in process algebra of the distributed control of track vehicles—A case study….Pages 192-205
Design verification of a microprocessor using branching time regular temporal logic….Pages 206-219
A case study in safety-critical design….Pages 220-233
Automatic reduction in CTL compositional model checking….Pages 234-247
Compositional model checking for linear-time temporal logic….Pages 248-259
Property preserving simulations….Pages 260-273
Verification with real-time COSPAN….Pages 274-287
Model-checking for real-time systems specified in Lotos….Pages 288-301
Decidability of bisimulation equivalences for parallel timer processes….Pages 302-315
A proof assistant for symbolic model-checking….Pages 316-329
Tableau recycling….Pages 330-342
Crocos: An integrated environment for interactive verification of SDL specifications….Pages 343-356
Verifying general safety and liveness properties with integer programming….Pages 357-369
Generating diagnostic information for behavioral preorders….Pages 370-383
A verification procedure via invariant for extended communicating finite-state machines….Pages 384-395
Efficient ω-regular language containment….Pages 396-409
Faster model checking for the modal Mu-Calculus….Pages 410-422