دانلود کتاب Computer Aided Verification: Fourth International Workshop, CAV '92 Montreal, Canada, June 29 – July 1, 1992 Proceedings

فهرست مطالب :

Computer-hindered verification (humans can do it too)....Pages 1-1
Modular abstractions for verifying real-time distributed systems....Pages 2-15
Layering techniques for development of parallel systems....Pages 16-29
Efficient local correctness checking....Pages 30-43
Mechanical verification of concurrent systems with TLA....Pages 44-55
Using a theorem prover for reasoning about concurrent algorithms....Pages 56-68
Verifying a logic synthesis tool in Nuprl: A case study in software verification....Pages 69-81
Higher-level specification and verification with BDDs....Pages 82-95
Symbolic bisimulation minimisation....Pages 96-108
Towards a verification technique for large synchronous circuits....Pages 109-122
Verifying timed behavior automata with nonbinary delay constraints....Pages 123-136
Timing verification by successive approximation....Pages 137-150
A verification strategy for timing constrained systems....Pages 151-163
Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits....Pages 164-177
State space caching revisited....Pages 178-191
Verification in process algebra of the distributed control of track vehicles—A case study....Pages 192-205
Design verification of a microprocessor using branching time regular temporal logic....Pages 206-219
A case study in safety-critical design....Pages 220-233
Automatic reduction in CTL compositional model checking....Pages 234-247
Compositional model checking for linear-time temporal logic....Pages 248-259
Property preserving simulations....Pages 260-273
Verification with real-time COSPAN....Pages 274-287
Model-checking for real-time systems specified in Lotos....Pages 288-301
Decidability of bisimulation equivalences for parallel timer processes....Pages 302-315
A proof assistant for symbolic model-checking....Pages 316-329
Tableau recycling....Pages 330-342
Crocos: An integrated environment for interactive verification of SDL specifications....Pages 343-356
Verifying general safety and liveness properties with integer programming....Pages 357-369
Generating diagnostic information for behavioral preorders....Pages 370-383
A verification procedure via invariant for extended communicating finite-state machines....Pages 384-395
Efficient ω-regular language containment....Pages 396-409
Faster model checking for the modal Mu-Calculus....Pages 410-422