Peter Lee (auth.), Hubert Garavel, John Hatcliff (eds.)3540008985, 9783540008989
The 43 revised full papers presented were carefully reviewed and selected from 160 submissions. The papers are organized in topical sections on bounded model checking and SAT-based methods, mu-calculus and temporal logics, verification of parameterized systems, abstractions and counterexamples, real-time and scheduling, security and cryptography, modules and compositional verification, symbolic state spaces and decision diagrams, performance and mobility, state space reductions, constraint solving and decision procedures, and testing and verification.
Table of contents :
What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying Code….Pages 1-1
Automatic Abstraction without Counterexamples….Pages 2-17
Bounded Model Checking for Past LTL….Pages 18-33
Experimental Analysis of Different Techniques for Bounded Model Checking….Pages 34-48
On the Universal and Existential Fragments of the μ-Calculus….Pages 49-64
Resets vs. Aborts in Linear Temporal Logic….Pages 65-80
A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems….Pages 81-96
Decidability of Invariant Validation for Paramaterized Systems….Pages 97-112
Verification and Improvement of the Sliding Window Protocol….Pages 113-127
Simple Representative Instantiations for Multicast Protocols….Pages 128-143
Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols….Pages 144-159
Proof-Like Counter-Examples….Pages 160-175
Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation….Pages 176-191
Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement….Pages 192-207
Counter-Example Guided Predicate Abstraction of Hybrid Systems….Pages 208-223
Schedulability Analysis Using Two Clocks….Pages 224-239
On Optimal Scheduling under Uncertainty….Pages 240-253
Static Guard Analysis in Timed Automata Verification….Pages 254-270
Moby /DC – A Tool for Model-Checking Parametric Real-Time Specifications….Pages 271-277
√erics: A Tool for Verifying Timed Automata and Estelle Specifications….Pages 278-283
A New Knowledge Representation Strategy for Cryptographic Protocol Analysis….Pages 284-298
Pattern-Based Abstraction for Verifying Secrecy in Protocols….Pages 299-314
Compositional Analysis for Verification of Parameterized Systems….Pages 315-330
Learning Assumptions for Compositional Verification….Pages 331-346
Automated Module Composition….Pages 347-362
Modular Strategies for Recursive Game Graphs….Pages 363-378
Saturation Unbound….Pages 379-393
Construction of Efficient BDDs for Bounded Arithmetic Constraints….Pages 394-408
Modeling and Analysis of Power-Aware Systems….Pages 409-424
A Set of Performance and Dependability Analysis Components for CADP….Pages 425-430
The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems….Pages 431-436
Banana – A Tool for Boundary Ambients Nesting ANAlysis….Pages 437-441
State Class Constructions for Branching Analysis of Time Petri Nets….Pages 442-457
Branching Processes of High-Level Petri Nets….Pages 458-472
Using Petri Net Invariants in State Space Construction….Pages 473-488
Optimistic Synchronization-Based State-Space Reduction….Pages 489-504
Checking Properties of Heap-Manipulating Procedures with a Constraint Solver….Pages 505-520
An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic….Pages 521-536
Strategies for Combining Decision Procedures….Pages 537-552
Generalized Symbolic Execution for Model Checking and Testing….Pages 553-568
Code-Based Test Generation for Validation of Functional Processor Descriptions….Pages 569-584
Large State Space Visualization….Pages 585-590
Automatic Test Generation with AGATHA….Pages 591-596
LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios….Pages 597-601
Reviews
There are no reviews yet.