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

Somesh Jha, Stefan Schwoon, Hao Wang, Thomas Reps (auth.), Holger Hermanns, Jens Palsberg (eds.)3540330569, 9783540330561

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.

---

Table of contents :
Front Matter….Pages –
Weighted Pushdown Systems and Trust-Management Systems….Pages 1-26
Automatic Verification of Parameterized Data Structures….Pages 27-41
Parameterized Verification of π -Calculus Systems….Pages 42-57
Easy Parameterized Verification of Biphase Mark and 8N1 Protocols….Pages 58-72
Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs….Pages 73-89
New Metrics for Static Variable Ordering in Decision Diagrams….Pages 90-104
Widening ROBDDs with Prime Implicants….Pages 105-119
Efficient Guided Symbolic Reachability Using Reachability Expressions….Pages 120-134
SDSAT : Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver….Pages 135-150
SAT-Based Software Certification….Pages 151-166
Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants….Pages 167-181
Exploration of the Capabilities of Constraint Programming for Software Verification….Pages 182-196
Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation Systems….Pages 197-211
Why Waste a Perfectly Good Abstraction?….Pages 212-226
Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking….Pages 227-241
Approximating Predicate Images for Bit-Vector Logic….Pages 242-256
Finitary Winning in ω -Regular Games….Pages 257-271
Efficient Model Checking for LTL with Partial Order Snapshots….Pages 272-286
A Local Shape Analysis Based on Separation Logic….Pages 287-302
Compositional Model Extraction for Higher-Order Concurrent Programs….Pages 303-317
A Region Graph Based Approach to Termination Proofs….Pages 318-333
Verifying Concurrent Message-Passing C Programs with Recursive Calls….Pages 334-349
Automata-Based Verification of Programs with Tree Updates….Pages 350-364
An Experimental Comparison of the Effectiveness of Control Flow Based Testing Approaches on Seeded Faults….Pages 365-378
Exploiting Traces in Program Analysis….Pages 379-393
Model-Checking Markov Chains in the Presence of Uncertainties….Pages 394-410
Safety Metric Temporal Logic Is Fully Decidable….Pages 411-425
Simulation-Based Graph Similarity….Pages 426-440
PRISM: A Tool for Automatic Verification of Probabilistic Systems….Pages 441-444
DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation….Pages 445-449
mcmas : A Model Checker for Multi-agent Systems….Pages 450-454
MSCan  – A Tool for Analyzing MSC Specifications….Pages 455-458
A Practical and Complete Approach to Predicate Refinement….Pages 459-473
Counterexample Driven Refinement for Abstract Interpretation….Pages 474-488
Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems….Pages 489-503
Back Matter….Pages –