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

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 -