Computer Aided Verification: 8th International Conference, Cav '96, New Brunswick, Nj, Usa, July 31 - August 3, 1996. Proceedings

ISBN-13: 9783540614746 / Angielski / Miękka / 1996 / 479 str.

R. Alur; T. A. Henzinger; Rajeev Alur

Opis

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.

Spis treści

Symbolic verification of communication protocols with infinite state spaces using QDDs.- A conjunctively decomposed boolean representation for symbolic model checking.- Symbolic model checking using algebraic geometry.- A partition refinement algorithm for the ?-calculus.- Polynomial time algorithms for testing probabilistic bisimulation and simulation.- Pushdown processes: Games and model checking.- Module checking.- Automatic verification of parameterized synchronous systems.- HORNSAT, model checking, verification and games.- Verifying the SRT division algorithm using theorem proving techniques.- Modular verification of SRT division.- Mechanically verifying a family of multiplier circuits.- Verifying systems with replicated components in mur?.- Verification of arithmetic circuits by comparing two similar circuits.- Automated deduction and formal methods.- A platform for combining deductive with algorithmic verification.- Verifying invariants using theorem proving.- Deductive model checking.- Automated verification by induction with associative-commutative operators.- Analysis of timed systems based on time-abstracting bisimulations.- Verification of an Audio Protocol with bus collision using Uppaal.- Selective quantitative analysis and interval model checking: Verifying different facets of a system.- Verifying continuous time Markov chains.- Verifying safety properties of differential equations.- Temporal verification by diagram transformations.- Protocol verification by aggregation of distributed transactions.- Atomicity refinement and trace reduction theorems.- Powerful techniques for the automatic generation of invariants.- Saving space by fully exploiting invisible transitions.- Using on-the-fly verification techniques for the generation of test suites.- Automatic translation of natural language system specifications into temporal logic.- Verification of fair transition systems.- The state of Spin.- The Mur ? verification system.- The NCSU Concurrency Workbench.- The Concurrency Factory: A development environment for concurrent systems.- XVERSA: An integrated graphical and textual toolset for the specification and analysis of resource-bound real-time systems.- EVP: Integration of FDTs for the analysis and verification of communication protocols.- PVS: Combining specification, proof checking, and model checking.- STeP: Deductive-algorithmic verification of reactive and real-time systems.- Symbolic model checking.- COSPAN.- VIS: A system for verification and synthesis.- MDG tools for the verification of RTL designs.- CADP a protocol validation and verification toolbox.- The FC2TOOLS set.- The Real-Time Graphical Interval Logic toolset.- The METAFrame'95 environment.- Verification Support Environment.- Marrella: A tool for simulation and verification.- Verifying the safety of a practical concurrent garbage collector.- Verification by behaviour abstraction.