Computer aided verification : 3rd international workshop, CAV '91, Aalborg, Denmark, July 1-4, 1991 : proceedings
Author(s)
Bibliographic Information
Computer aided verification : 3rd international workshop, CAV '91, Aalborg, Denmark, July 1-4, 1991 : proceedings
(Lecture notes in computer science, 575)
Springer-Verlag, c1992
- : gw
- : us
Available at 58 libraries
  Aomori
  Iwate
  Miyagi
  Akita
  Yamagata
  Fukushima
  Ibaraki
  Tochigi
  Gunma
  Saitama
  Chiba
  Tokyo
  Kanagawa
  Niigata
  Toyama
  Ishikawa
  Fukui
  Yamanashi
  Nagano
  Gifu
  Shizuoka
  Aichi
  Mie
  Shiga
  Kyoto
  Osaka
  Hyogo
  Nara
  Wakayama
  Tottori
  Shimane
  Okayama
  Hiroshima
  Yamaguchi
  Tokushima
  Kagawa
  Ehime
  Kochi
  Fukuoka
  Saga
  Nagasaki
  Kumamoto
  Oita
  Miyazaki
  Kagoshima
  Okinawa
  Korea
  China
  Thailand
  United Kingdom
  Germany
  Switzerland
  France
  Belgium
  Netherlands
  Sweden
  Norway
  United States of America
Note
Includes bibliographical references
Description and Table of Contents
Description
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.- Silence is golden: Branching bisimilarity is decidable for context-free processes.- Computing distinguishing formulas for branching bisimulation.- Compositional checking of satisfaction.- An action based framework for verifying logical and behavioural properties of concurrent systems.- A linear-time model-checking algorithm for the alternation-free modal mu-calculus.- Automatic temporal verification of buffer systems.- Mechanically checked proofs of kernel specifications.- A top down approach to the formal specification of SCI cache coherence.- Integer programming in the analysis of concurrent systems.- The lotos model of a fault protected system and its verification using a petri net based approach.- Error diagnosis in finite communicating systems.- Temporal precondition verification of design transformations.- PAM: A process algebra manipulator.- The Concurrency Workbench with priorities.- A proof assistant for PSF.- Avoiding state explosion by composition of minimal covering graphs.- "On the fly" verification of behavioural equivalences and preorders.- Bounded-memory algorithms for verification on-the-fly.- Generating BDDs for symbolic model checking in CCS.- Vectorized symbolic model checking of computation tree logic for sequential machine verification.- Functional extension of symbolic model checking.- An automated proof technique for finite-state machine equivalence.- From data structure to process structure.- Checking for language inclusion using simulation preorders.- A semantic driven method to check the fineteness of CCS processes.- Using the HOL prove assistant for proving the correctness of term rewriting rules reducing terms of sequential behavior.- Mechanizing a proof by induction of process algebra specifications in higher order logic.- A two-level formal verification methodology using HOL and COSMOS.- Efficient algorithms for verification of equivalences for probabilistic processes.- Partial-order model checking: A guide for the perplexed.- Using partial orders for the efficient verification of deadlock freedom and safety properties.- Complexity results for POMSET languages.- Mechanically verifying safety and liveness properties of delay insensitive circuits.- Automating most parts of hardware proofs in HOL.- An overview and synthesis on timed process algebras.- Minimum and maximum delay problems in realtime systems.- Formal verification of speed-dependent asynchronous circuits using symbolic model checking of Branching Time Regular Temporal Logic.- Verifying properties of HMS machine specifications of real-time systems.- A linear time process algebra.- Deciding properties of regular real timed processes.- An algebra of Boolean processes.- Comparing generic state machines.- An automata theoretic approach to Temporal Logic.
by "Nielsen BookData"