Computer Aided Verification: Fourth International Workshop, CAV '92, Montreal, Canada, June 29 - July 1, 1992. ProceedingsGregor 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 |
طبعات أخرى - عرض جميع المقتطفات
عبارات ومصطلحات مألوفة
abstraction action algorithm atomic propositions automata automaton behavior bisimulation block control Boolean Equation System cache checker circuit component composition Computer Science concurrent systems consistency contains corresponding defined definition delay constraint denote described dopar E.M. Clarke edge encoding example Figure finite finite-state fixpoint formal formal verification formula function given global graph implementation inequalities infinite input interval L-process labelled transition system language layer Lemma linear linear temporal logic Lotos M₁ machine method model checking module node Nuprl operator output P₁ parametric Boolean expressions path Petri nets predicate preorder problem proof properties protocol prove pull-back push-away reachable recursive rules satisfies semantics sequence sequential sleep sets specification strongly connected components symbolic model checking symbolic simulation tableau technique temporal logic theorem timer transition relation transitive closure U₁ unfolding variables vectors vehicle verification well-foundedness