Computer Aided Verification: 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27–31, 2002 Proceedings

Gerard_J. Holzmann (auth.), Ed Brinksma, Kim Guldstrand Larsen (eds.)3540439978, 9783540439974

This volume contains the proceedings of the conference on Computer Aided V- i?cation (CAV 2002), held in Copenhagen, Denmark on July 27-31, 2002. CAV 2002 was the 14th in a series of conferences dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical – sults to concrete applications, with an emphasis on practical veri?cation tools, including algorithms and techniques needed for their implementation. The c- ference has traditionally drawn contributions from researchers as well as prac- tioners in both academia and industry. This year we received 94 regular paper submissions out of which 35 were selected. Each submission received an average of 4 referee reviews. In addition, the CAV program contained 11 tool presentations selected from 16 submissions. For each tool presentation, a demo was given at the conference. The large number of tool submissions and presentations testi?es to the liveliness of the ?eld and its applied ?avor.

---

Table of contents :
Software Analysis and Model Checking….Pages 1-16
The Quest for Efficient Boolean Satisfiability Solvers….Pages 17-36
On Abstraction in Software Verification….Pages 37-56
The Symbolic Approach to Hybrid Systems….Pages 57-57
Infinite Games and Verification….Pages 58-65
Symbolic Localization Reduction with Reconstruction Layering and Backtracking….Pages 65-77
Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions….Pages 78-92
Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking….Pages 93-106
Liveness with (0,1, ∞)- Counter Abstraction….Pages 107-122
Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking….Pages 123-136
Automatic Abstraction Using Generalized Model Checking….Pages 137-151
Property Checking via Structural Analysis….Pages 151-165
Conformance Checking for Models of Asynchronous Message Passing Software….Pages 166-179
A Modular Checker for Multithreaded Programs….Pages 180-194
Automatic Derivation of Timing Constraints by Failure Analysis….Pages 195-208
Deciding Separation Formulas with SAT….Pages 209-222
Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling….Pages 223-235
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT….Pages 236-249
Applying SAT Methods in Unbounded Symbolic Model Checking….Pages 250-264
SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques….Pages 265-279
Semi-formal Bounded Model Checking….Pages 280-294
Algorithmic Verification of Invalidation-Based Protocols….Pages 295-308
Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving….Pages 309-323
Automated Unbounded Verification of Security Protocols….Pages 324-337
Exploiting Behavioral Hierarchy for Efficient Model Checking….Pages 338-342
IF-2.0: A Validation Environment for Component-Based Real-Time Systems….Pages 343-348
The AVISS Security Protocol Analysis Tool….Pages 349-354
SPeeDI — A Verification Tool for Polygonal Hybrid Systems….Pages 354-359
NuSMV 2: An OpenSource Tool for Symbolic Model Checking….Pages 359-364
The d/dt Tool for Verification of Hybrid Systems….Pages 365-370
Model Checking Linear Properties of Prefix-Recognizable Systems….Pages 371-385
Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking….Pages 386-400
On Discrete Modeling and Model Checking for Nonlinear Analog Systems….Pages 401-414
Synchronous and Bidirectional Component Interfaces….Pages 414-427
Interface Compatibility Checking for Software Modules….Pages 428-441
Practical Methods for Proving Program Termination….Pages 442-454
Evidence-Based Model Checking….Pages 455-470
Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification….Pages 471-484
Vacuum Cleaning CTL Formulae….Pages 485-499
CVC: A Cooperating Validity Checker….Pages 500-504
ΧChek: A Multi-valued Model-Checker….Pages 505-509
PathFinder: A Tool for Design Exploration….Pages 510-514
Abstracting C with abC….Pages 515-520
AMC: An Adaptive Model Checker….Pages 521-525
Temporal-Safety Proofs for Systems Code….Pages 526-538
Extrapolating Tree Transformations….Pages 539-554
Regular Tree Model Checking….Pages 555-568
Compressing Transitions for Model Checking….Pages 569-582
Canonical Prefixes of Petri Net Unfoldings….Pages 582-595
State Space Reduction by Proving Confluence….Pages 596-609
Fair Simulation Minimization….Pages 610-623