Computer aided verification : 15th international conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003 : proceedings
Salvato in:
| Ente Autore: | |
|---|---|
| Altri autori: | , |
| Natura: | Livre numérique |
| Lingua: | Anglais |
| Pubblicazione: |
Berlin [etc.] :
Springer
201X.
Berlin [etc.] : |
| Serie: | Lecture notes in computer science
2725 |
| Soggetti: | |
| Accesso online: | Accès sur la plateforme de l'éditeur Accès Université d'Orléans Accès INSA CVL |
| Nota: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Computer aided verification, 15th international conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, proceedings, Warren A. Hunt, Jr., Fabio Somenzi (eds.), Berlin, Springer, 2003, 1 vol. (XII-462 p.), Lecture notes in computer science, 3-540-40524-0 • Computer Aided Verification, Texte imprimé, 9783662186855 |
Sommario:
- 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.