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 2003, Proceedings

by Tacas 200 (2003 Warsaw, Poland); Garavel, Hubert; Hatcliff, John

• ISBN13: 9783540008989
• ISBN10: 3540008985
• Format: Paperback
• Copyright: 2003-05-01
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2003, held in Warsaw, Poland, in April 2003. 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

Invited Contributions
What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying Code	p. 1
Bounded Model Checking and SAT-Based Methods
Automatic Abstraction without Counterexamples	p. 2
Bounded Model Checking for Past LTL	p. 18
Experimental Analysis of Different Techniques for Bounded Model Checking	p. 34
Mu-Calculus and Temporal Logics
On the Universal and Existential Fragments of the ¿-Calculus	p. 49
Resets vs. Aborts in Linear Temporal Logic	p. 65
A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems	p. 81
Verification of Parameterized Systems
Decidability of Invariant Validation for Paramaterized Systems	p. 97
Verification and Improvement of the Sliding Window Protocol	p. 113
Simple Representative Instantiations for Multicast Protocols	p. 128
Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols	p. 144
Abstractions and Counter-Examples
Proof-Like Counter-Examples	p. 160
Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation	p. 176
Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement	p. 192
Counter-Example Guided Predicate Abstraction of Hybrid Systems	p. 208
Real-Time and Scheduling
Schedulability Analysis Using Two Clocks	p. 224
On Optimal Scheduling under Uncertainty	p. 240
Static Guard Analysis in Timed Automata Verification	p. 254
Moby/DC-A Tool for Model-Checking Parametric Real-Time Specifications	p. 271
√erics: A Tool for Verifying Timed Automata and Estelle Specifications	p. 278
Security and Cryptography
A New Knowledge Representation Strategy for Cryptographic Protocol Analysis	p. 284
Pattern-Based Abstraction for Verifying Secrecy in Protocols	p. 299
Modules and Compositional Verification
Compositional Analysis for Verification of Parameterized Systems	p. 315
Learning Assumptions for Compositional Verification	p. 331
Automated Module Composition	p. 347
Modular Strategies for Recursive Game Graphs	p. 363
Symbolic State Spaces and Decision Diagrams
Saturation Unbound	p. 379
Construction of Efficient BDDs for Bounded Arithmetic Constraints	p. 394
Performance and Mobility
Modeling and Analysis of Power-Aware Systems	p. 409
A Set of Performance and Dependability Analysis Components for CADP	p. 425
The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems	p. 431
Banana - A Tool for Boundary Ambients Nesting ANAlysis	p. 437
State Space Reductions
State Class Constructions for Branching Analysis of Time Petri Nets	p. 442
Branching Processes of High-Level Petri Nets	p. 458
Using Petri Net Invariants in State Space Construction	p. 473
Optimistic Synchronization-Based State-Space Reduction	p. 489
Constraint-Solving and Decision Procedures
Checking Properties of Heap-Manipulating Procedures with a Constraint Solver	p. 505
An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic	p. 521
Strategies for Combining Decision Procedures	p. 537
Testing and Verification
Generalized Symbolic Execution for Model Checking and Testing	p. 553
Code-Based Test Generation for Validation of Functional Processor Descriptions	p. 569
Large State Space Visualization	p. 585
Automatic Test Generation with AGATHA	p. 591
LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios	p. 597
Author Index	p. 603
Table of Contents provided by Publisher. All Rights Reserved.