Computer Aided Verification 3rd International Workshop, CAV '91, Aalborg, Denmark, July 1-4, 1991. Proceedings

Computer Aided Verification 3rd International Workshop, CAV '91, Aalborg, Denmark, July 1-4, 1991. Proceedings / edited by Kim G. Larsen, Arne Skou.

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 metho...

Full description

Saved in:
Bibliographic Details
Corporate Author: SpringerLink (Online service)
Other Authors: Larsen, Kim G. (Editor), Skou, Arne (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1992.
Edition:1st ed. 1992.
Series:Lecture Notes in Computer Science, 575
Springer eBook Collection.
Subjects:
Computers.
Software engineering.
Architecture, Computer.
Computer logic.
Mathematical logic.
Special purpose computers.
Electronic resources (E-books)
Online Access:Click to view e-book
Holy Cross Note:Loaded electronically.
Electronic access restricted to members of the Holy Cross Community.
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.

Similar Items