Computer Aided Verification: Fourth International Workshop, CAV '92, Montreal, Canada, June 29 - July 1, 1992. Proceedings

الغلاف الأمامي
Gregor von Bochmann, David K. Probst
Springer Science & Business Media, 30‏/03‏/1993 - 422 من الصفحات
This volume gives the proceedings of the Fourth Workshop on Computer-Aided Verification (CAV '92), held in Montreal, June 29 - July 1, 1992. 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 the computer-aided verification of concurrent systems. The workshops provide an opportunity for comparing various verification methods and practical tools that can be used to assist the applications designer. Emphasis is placed on new research results and the application of existing results to real verification problems. The volume contains 31 papers selected from 75 submissions. These are organized into parts on reduction techniques, proof checking, symbolic verification, timing verification, partial-order approaches, case studies, model and proof checking, and other approaches. The volume starts with an invited lecture by Leslie Lamport entitled "Computer-hindered verification (humans can do it too)".
 

الصفحات المحددة

المحتوى

ComputerHindered Verification Humans Can Do It Too
1
Modular Abstractions for Verifying RealTime Distributed Systems
2
Layering Techniques for Development of Parallel Systems
16
Efficient Local Correctness Checking
30
Mechanical Verification of Concurrent Systems with TLA
44
Using a Theorem Prover for Reasoning about Concurrent Algorithms
56
A Case Study in Software Verification
69
HigherLevel Specification and Verification With BDDs
82
A Case Study in SafetyCritical Design
220
Automatic Reduction in CTL Compositional Model Checking
234
Compositional Model Checking for LinearTime Temporal Logic
248
Property preserving simulations
260
Verification with RealTime COSPAN
274
Modelchecking for realtime systems specified in Lotos
288
Decidability of Bisimulation Equivalences for Parallel Timer Processes
302
A Proof Assistant for Symbolic ModelChecking
316

Symbolic Bisimulation Minimisation
96
Towards A Verification Technique for Large Synchronous Circuits
109
Verifying Timed Behavior Automata with Nonbinary Delay Constraints
123
Timing Verification by Successive Approximation
137
A Verification Strategy for Timing Constrained Systems
151
Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits
164
State Space Caching Revisited
178
Verification in process algebra of the distributed control of track vehiclesA case study
192
Design Verification of a Microprocessor Using Branching Time Regular Temporal Logic
206
Tableau Recycling
330
AN INTEGRATED ENVIRONMENT FOR INTERACTIVE VERIFICATION OF SDL SPECIFICATIONS
343
Verifying General Safety and Liveness Properties With Integer Programming
357
Generating Diagnostic Information for Behavioral Preorders
370
A Verification Procedure via Invariant for Extended Communicating FiniteState Machines
384
Efficient coRegular Language Containment
396
Faster Model Checking for the Modal MuCalculus
410
حقوق النشر

طبعات أخرى - عرض جميع المقتطفات

عبارات ومصطلحات مألوفة

معلومات المراجع