Computer Aided Verification: 15th International Conference, Cav 2003, Boulder, Co, Usa, July 8-12, 2003, Proceedings

ISBN-13: 9783540405245 / Angielski / Miękka / 2003 / 462 str.

Jr. Hunt; Fabio Somenzi

Opis

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.

Spis treści

Extending Bounded Model Checking.- Interpolation and SAT-Based Model Checking.- Bounded Model Checking and Induction: From Refutation to Verification.- Symbolic Model Checking.- Reasoning with Temporal Logic on Truncated Paths.- Structural Symbolic CTL Model Checking of Asynchronous Systems.- A Work-Efficient Distributed Algorithm for Reachability Analysis.- Games, Trees, and Counters.- Modular Strategies for Infinite Games on Recursive Graphs.- Fast Mu-Calculus Model Checking when Tree-Width Is Bounded.- Dense Counter Machines and Verification Problems.- Tool Presentations I.- TRIM: A Tool for Triggered Message Sequence Charts.- Model Checking Multi-Agent Programs with CASP.- Monitoring Temporal Rules Combined with Time Series.- FAST: Fast Acceleration of Symbolic Transition Systems.- Rabbit: A Tool for BDD-Based Verification of Real-Time Systems.- Abstraction I.- Making Predicate Abstraction Efficient:.- A Symbolic Approach to Predicate Abstraction.- Unbounded, Fully Symbolic Model Checking of Timed Automata Using Boolean Methods.- Dense Time.- Digitizing Interval Duration Logic.- Timed Control with Partial Observability.- Hybrid Acceleration Using Real Vector Automata.- Tool Presentations II.- Abstraction and BDDs Complement SAT-Based BMC in DiVer.- TLQSolver: A Temporal Logic Query Checker.- Evidence Explorer: A Tool for Exploring Model-Checking Proofs.- HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols.- Infinite State Systems.- Iterating Transducers in the Large.- Algorithmic Improvements in Regular Model Checking.- Efficient Image Computation in Infinite State Model Checking.- Abstraction II.- Thread-Modular Abstraction Refinement.- A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement.- Abstraction for Branching Time Properties.- Applications.- Certifying Optimality of State Estimation Programs.- Domain-Specific Optimization in Automata Learning.- Model Checking Conformance with Scenario-Based Specifications.- Theorem Proving.- Deductive Verification of Advanced Out-of-Order Microprocessors.- Theorem Proving Using Lazy Proof Explication.- Automata-Based Verification.- Enhanced Vacuity Detection in Linear Temporal Logic.- Bridging the Gap between Fair Simulation and Trace Inclusion.- An Improved On-the-Fly Tableau Construction for a Real-Time Temporal Logic.- Invariants.- Strengthening Invariants by Symbolic Consistency Testing.- Linear Invariant Generation Using Non-linear Constraint Solving.- Explicit Model Checking.- To Store or Not to Store.- Calculating ?-Confluence Compositionally.