Computer Aided Verification: 8th International Conference, CAV ’96 New Brunswick, NJ, USA, July 31– August 3, 1996 Proceedings

Bernard Boigelot, Patrice Godefroid (auth.), Rajeev Alur, Thomas A. Henzinger (eds.)3540614745, 9783540614746

This book constitutes the refereed proceedings of the 8th International Conference on Computer Aided Verification, CAV ’96, held in New Brunswick, NJ, USA, in July/August 1996 as part of the FLoC ’96 federated conference.
The volume presents 32 revised full research contributions selected from a total of 93 submissions; also included are 20 carefully selected descriptions of tools and case studies. The set of papers reports the state-of-the-art of the theory and practice of computer assisted formal analysis methods for software and hardware systems; a certain emphasis is placed on verification tools and the algorithms and techniques that are needed for their implementation.

---

Table of contents :
Symbolic verification of communication protocols with infinite state spaces using QDDs….Pages 1-12
A conjunctively decomposed boolean representation for symbolic model checking….Pages 13-25
Symbolic model checking using algebraic geometry….Pages 26-37
A partition refinement algorithm for the π-calculus….Pages 38-49
Polynomial time algorithms for testing probabilistic bisimulation and simulation….Pages 50-61
Pushdown processes: Games and model checking….Pages 62-74
Module checking….Pages 75-86
Automatic verification of parameterized synchronous systems….Pages 87-98
HORNSAT, model checking, verification and games….Pages 99-110
Verifying the SRT division algorithm using theorem proving techniques….Pages 111-122
Modular verification of SRT division….Pages 123-134
Mechanically verifying a family of multiplier circuits….Pages 135-146
Verifying systems with replicated components in murϕ….Pages 147-158
Verification of arithmetic circuits by comparing two similar circuits….Pages 159-168
Automated deduction and formal methods….Pages 169-183
A platform for combining deductive with algorithmic verification….Pages 184-195
Verifying invariants using theorem proving….Pages 196-207
Deductive model checking….Pages 208-219
Automated verification by induction with associative-commutative operators….Pages 220-231
Analysis of timed systems based on time-abstracting bisimulations….Pages 232-243
Verification of an Audio Protocol with bus collision using Uppaal ….Pages 244-256
Selective quantitative analysis and interval model checking: Verifying different facets of a system….Pages 257-268
Verifying continuous time Markov chains….Pages 269-276
Verifying safety properties of differential equations….Pages 277-287
Temporal verification by diagram transformations….Pages 288-299
Protocol verification by aggregation of distributed transactions….Pages 300-310
Atomicity refinement and trace reduction theorems….Pages 311-322
Powerful techniques for the automatic generation of invariants….Pages 323-335
Saving space by fully exploiting invisible transitions….Pages 336-347
Using on-the-fly verification techniques for the generation of test suites….Pages 348-359
Automatic translation of natural language system specifications into temporal logic….Pages 360-371
Verification of fair transition systems….Pages 372-382
The state of Spin….Pages 383-389
The Mur ϕ verification system….Pages 390-393
The NCSU Concurrency Workbench….Pages 394-397
The Concurrency Factory: A development environment for concurrent systems….Pages 398-401
XVERSA: An integrated graphical and textual toolset for the specification and analysis of resource-bound real-time systems….Pages 402-405
EVP: Integration of FDTs for the analysis and verification of communication protocols….Pages 406-410
PVS: Combining specification, proof checking, and model checking….Pages 411-414
STeP: Deductive-algorithmic verification of reactive and real-time systems….Pages 415-418
Symbolic model checking….Pages 419-422
COSPAN….Pages 423-427
VIS: A system for verification and synthesis….Pages 428-432
MDG tools for the verification of RTL designs….Pages 433-436
CADP a protocol validation and verification toolbox….Pages 437-440
The FC2TOOLS set….Pages 441-445
The Real-Time Graphical Interval Logic toolset….Pages 446-449
The METAFrame’95 environment….Pages 450-453
Verification Support Environment….Pages 454-457
Marrella: A tool for simulation and verification….Pages 458-461
Verifying the safety of a practical concurrent garbage collector….Pages 462-465
Verification by behaviour abstraction….Pages 466-469