Computer Aided Verification: 5th International Conference, CAV '93 Elounda, Greece, June 28–July 1, 1993 Proceedings

Logic synthesis and design verification....Pages 1-2
Efficient verification with BDDs using implicitly conjoined invariants....Pages 3-14
Parametric circuit representation using inductive Boolean functions....Pages 15-28
An iterative approach to language containment....Pages 29-40
BDD-Based debugging of designs using language containment and fair CTL....Pages 41-58
Reliable hashing without collision detection....Pages 59-70
A tool for symbolic program verification and abstraction....Pages 71-84
Symbolic equivalence checking....Pages 85-96
A decision algorithm for full propositional temporal logic....Pages 97-109
Reachability and recurrence in Extended Finite State Machines: Modular Vector Addition Systems....Pages 110-122
Automatic generation of network invariants for the verification of iterative sequential systems....Pages 123-137
A Graphical Interval Logic toolset for verifying concurrent systems....Pages 138-153
Combining model checking and theorem proving to verify parallel processes....Pages 154-165
Verification of a multiplier: 64 bits and beyond....Pages 166-179
Protocol design for an automated highway system....Pages 180-180
Computing accumulated delays in real-time systems....Pages 181-193
Reachability analysis of planar multi-linear systems....Pages 194-209
An efficient algorithm for minimizing real-time transition systems....Pages 210-224
Verification of timing properties of VHDL....Pages 225-236
Alternating RQ timed automata....Pages 237-252
Timed modal specification — Theory and tools....Pages 253-267
A mechanically verified application for a mechanically verified environment....Pages 268-279
Verification of real-time systems using PVS....Pages 280-291
The formal verification of an algorithm for interactive consistency under a hybrid fault model....Pages 292-304
Computer-assisted simulation proofs....Pages 305-319
A verifier and timing analyser for simple imperative programs....Pages 320-320
Efficient verification of parallel real-time systems....Pages 321-332
Delay analysis in synchronous programs....Pages 333-346
Verifying quantitative real-time properties of synchronous programs....Pages 347-358
A modal logic for message passing processes....Pages 359-370
Functionality decomposition by compositional correctness preserving transformation....Pages 371-384
On model-checking for fragments of μ-calculus....Pages 385-396
On-the-fly verification with stubborn sets....Pages 397-408
All from one, one for all: on model checking using representatives....Pages 409-423
Verifying timed behavior automata with input/output critical races....Pages 424-437
Refining dependencies improves partial-order verification methods (extended abstract)....Pages 438-449
Exploiting symmetry in temporal logic model checking....Pages 450-462
Symmetry and model checking....Pages 463-478
Generation of reduced models for checking fragments of CTL....Pages 479-490
A Structural linearization principle for processes....Pages 491-504