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

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