Computer Aided Verification: 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003. Proceedings

Simon N. Foley (auth.), Warren A. Hunt Jr., Fabio Somenzi (eds.)3540405240, 9783540405245

This book constitutes the refereed proceedings of the 15th International Conference on Computer Aided Verification, CAV 2003, held in Boulder, CO, USA in July 2003.

The 32 revised full papers and 9 tool papers presented were carefully reviewed and selected from a total of 102 submissions. The papers are organized in topical sections on bounded model checking; symbolic model checking; games, trees, and counters; tools; abstraction; dense time; infinite state systems; applications; theorem proving; automata-based verification; invariants; and explicit model checking.

---

Table of contents :
Front Matter….Pages –
Interpolation and SAT-Based Model Checking….Pages 1-13
Bounded Model Checking and Induction: From Refutation to Verification….Pages 14-26
Reasoning with Temporal Logic on Truncated Paths….Pages 27-39
Structural Symbolic CTL Model Checking of Asynchronous Systems….Pages 40-53
A Work-Efficient Distributed Algorithm for Reachability Analysis….Pages 54-66
Modular Strategies for Infinite Games on Recursive Graphs….Pages 67-79
Fast Mu-Calculus Model Checking when Tree-Width Is Bounded….Pages 80-92
Dense Counter Machines and Verification Problems….Pages 93-105
TRIM: A Tool for Triggered Message Sequence Charts….Pages 106-109
Model Checking Multi-Agent Programs with CASP….Pages 110-113
Monitoring Temporal Rules Combined with Time Series….Pages 114-117
FAST: Fast Acceleration of Symbolic Transition Systems….Pages 118-121
Rabbit: A Tool for BDD-Based Verification of Real-Time Systems….Pages 122-125
Making Predicate Abstraction Efficient:….Pages 126-140
A Symbolic Approach to Predicate Abstraction….Pages 141-153
Unbounded, Fully Symbolic Model Checking of Timed Automata Using Boolean Methods….Pages 154-166
Digitizing Interval Duration Logic….Pages 167-179
Timed Control with Partial Observability….Pages 180-192
Hybrid Acceleration Using Real Vector Automata….Pages 193-205
Abstraction and BDDs Complement SAT-Based BMC in DiVer ….Pages 206-209
TLQSolver: A Temporal Logic Query Checker….Pages 210-214
Evidence Explorer: A Tool for Exploring Model-Checking Proofs….Pages 215-218
HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols….Pages 219-222
Iterating Transducers in the Large….Pages 223-235
Algorithmic Improvements in Regular Model Checking….Pages 236-248
Efficient Image Computation in Infinite State Model Checking….Pages 249-261
Thread-Modular Abstraction Refinement….Pages 262-274
A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement….Pages 275-287
Abstraction for Branching Time Properties….Pages 288-300
Certifying Optimality of State Estimation Programs….Pages 301-314
Domain-Specific Optimization in Automata Learning….Pages 315-327
Model Checking Conformance with Scenario-Based Specifications….Pages 328-340
Deductive Verification of Advanced Out-of-Order Microprocessors….Pages 341-354
Theorem Proving Using Lazy Proof Explication….Pages 355-367
Enhanced Vacuity Detection in Linear Temporal Logic….Pages 368-380
Bridging the Gap between Fair Simulation and Trace Inclusion….Pages 381-393
An Improved On-the-Fly Tableau Construction for a Real-Time Temporal Logic….Pages 394-406
Strengthening Invariants by Symbolic Consistency Testing….Pages 407-419
Linear Invariant Generation Using Non-linear Constraint Solving….Pages 420-432
To Store or Not to Store….Pages 433-445
Calculating τ -Confluence Compositionally….Pages 446-459
Back Matter….Pages –