Tools and Algorithms for the Construction and Analysis of Systems: 12th International Conference, TACAS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings

Front Cover
Springer Science & Business Media, Mar 15, 2006 - Computers - 506 pages
ETAPS 2006 was the ninth instance of the European Joint Conferences on Theory and Practice of Software. ETAPS is an annual federated conference that was established in 1998 by combining a number of existing and new conferences. This year it comprised ?ve conferences (CC, ESOP, FASE, FOSSACS, TACAS), 18 satellite workshops (AC- CAT, AVIS, CMCS, COCV, DCC, EAAI, FESCA, FRCSS, GT-VMT, LDTA, MBT, QAPL, SC, SLAP, SPIN, TERMGRAPH, WITS and WRLA), two tutorials, and seven invited lectures (not including those that were speci?c to the satellite events). We - ceived over 550 submissions to the ?ve conferences this year, giving an overall acc- tance rate of 23%, with acceptance rates below 30% for each conference. Congratu- tions to all the authors who made it to the ?nal programme! I hope that most of the other authorsstill founda way of participatingin this excitingevent and I hope you will continue submitting. The events that comprise ETAPS address various aspects of the system devel- ment process, including speci?cation, design, implementation, analysis and impro- ment. The languages, methodologies and tools which support these activities are all well within its scope. Di?erent blends of theory and practice are represented, with an inclination towards theory with a practical motivation on the one hand and soundly based practice on the other. Many of the issues involved in software design apply to systems in general, including hardware systems, and the emphasis on software is not intended to be exclusive.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Weighted Pushdown Systems and TrustManagement Systems
1
Automatic Verification of Parameterized Data Structures
27
Parameterized Verification of πCalculus Systems
42
Easy Parameterized Verification of Biphase Mark and 8N1 Protocols
58
Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent ObjectOriented Programs
73
New Metrics for Static Variable Ordering in Decision Diagrams
90
Widening ROBDDs with Prime Implicants
105
Efficient Guided Symbolic Reachability Using Reachability Expressions
120
Compositional Model Extraction for HigherOrder Concurrent Programs
303
A Region Graph Based Approach to Termination Proofs
318
Verifying Concurrent MessagePassing C Programs with Recursive Calls
334
AutomataBased Verification of Programs with Tree Updates
350
An Experimental Comparison of the Effectiveness of Control Flow Based Testing Approaches on Seeded Faults
365
Exploiting Traces in Program Analysis
379
ModelChecking Markov Chains in the Presence of Uncertainties
394
Safety Metric Temporal Logic Is Fully Decidable
411

Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver
135
SATBased Software Certification
151
Towards Combining SMT Solvers and Interactive Proof Assistants
167
Exploration of the Capabilities of Constraint Programming for Software Verification
182
CounterexampleGuided Abstraction Refinement for the Analysis of Graph Transformation Systems
197
Why Waste a Perfectly Good Abstraction?
212
Efficient Abstraction Refinement in InterpolationBased Unbounded Model Checking
227
Approximating Predicate Images for BitVector Logic
242
Finitary Winning in ωRegular Games
257
Efficient Model Checking for LTL with Partial Order Snapshots
272
A Local Shape Analysis Based on Separation Logic
287
SimulationBased Graph Similarity
426
A Tool for Automatic Verification of Probabilistic Systems
441
Tools for Distributed Explicit State Space Generation
445
A Model Checker for Multiagent Systems
450
MSCan A Tool for Analyzing MSC Specifications
455
A Practical and Complete Approach to Predicate Refinement
459
Counterexample Driven Refinement for Abstract Interpretation
474
Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems
489
Author Index
504
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information