Computer Aided Verification 5th International Conference, CAV'93, Elounda, Greece, June 28 - July 1, 1993. Proceedings
This volume contains the proceedings of the Fifth Conference on Computer-Aided Verfication, held in Crete, Greece, in June/July 1993. The objective of the CAV conferences is to bring together researchers and practitioners interested in the development anduse of methods, tools, and theories for the c...
| Other Authors: | |
|---|---|
| Format: | eBook |
| Language: | English |
| Published: |
Berlin, Heidelberg
Springer Berlin Heidelberg
1993, 1993
|
| Edition: | 1st ed. 1993 |
| Series: | Lecture Notes in Computer Science
|
| Subjects: | |
| Online Access: | |
| Collection: | Springer Book Archives -2004 - Collection details see MPG.ReNa |
Table of Contents:
- Computing accumulated delays in real-time systems
- Reachability analysis of planar multi-linear systems
- An efficient algorithm for minimizing real-time transition systems
- Verification of timing properties of VHDL
- Alternating RQ timed automata
- Timed modal specification — Theory and tools
- A mechanically verified application for a mechanically verified environment
- Verification of real-time systems using PVS
- The formal verification of an algorithm for interactive consistency under a hybrid fault model
- Computer-assisted simulation proofs
- A verifier and timing analyser for simple imperative programs
- Efficient verification of parallel real-time systems
- Delay analysis in synchronous programs
- Verifying quantitative real-time properties of synchronous programs
- A modal logic for message passing processes
- Functionality decomposition by compositional correctness preserving transformation
- On model-checking for fragments of ?-calculus
- On-the-fly verification with stubborn sets
- All from one, one for all: on model checking using representatives
- Verifying timed behavior automata with input/output critical races
- Refining dependencies improves partial-order verification methods (extended abstract)
- Exploiting symmetry in temporal logic model checking
- Symmetry and model checking
- Generation of reduced models for checking fragments of CTL
- A Structural linearization principle for processes
- Logic synthesis and design verification
- Efficient verification with BDDs using implicitly conjoined invariants
- Parametric circuit representation using inductive Boolean functions
- An iterative approach to language containment
- BDD-Based debugging of designs using language containment and fair CTL
- Reliable hashing without collision detection
- A tool for symbolic program verification and abstraction
- Symbolic equivalence checking
- A decision algorithm for full propositional temporal logic
- Reachability and recurrence in Extended Finite State Machines: Modular Vector Addition Systems
- Automatic generation of network invariants for the verification of iterative sequential systems
- A Graphical Interval Logic toolset for verifying concurrent systems
- Combining model checking and theorem proving to verify parallel processes
- Verification of a multiplier: 64 bits and beyond
- Protocol design for an automated highway system