دانلود کتاب Tools and Algorithms for the Construction and Analysis of Systems: 9th International Conference, TACAS 2003 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003 Warsaw, Poland, April 7–11, 2003 Proceedings

فهرست مطالب :

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