Computer Aided Verification 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings
| Other Authors: | , |
|---|---|
| Format: | eBook |
| Language: | English |
| Published: |
Berlin, Heidelberg
Springer Berlin Heidelberg
2003, 2003
|
| Edition: | 1st ed. 2003 |
| Series: | Lecture Notes in Computer Science
|
| Subjects: | |
| Online Access: | |
| Collection: | Springer Book Archives -2004 - Collection details see MPG.ReNa |
Table of Contents:
- 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
- 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