Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings

Yann Thierry-Mieg, Denis Poitrenaud, Alexandre Hamez, Fabrice Kordon (auth.), Stefan Kowalewski, Anna Philippou (eds.)3642007678, 9783642007675

This book constitutes the refereed proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009, held in York, UK, in March 2009, as part of ETAPS 2009, the European Joint Conferences on Theory and Practice of Software.

The 27 full papers and 8 tool demonstrations included in the volume were thoroughly reviewed and selected from 131 submissions. The papers are organized in topical sections on Model Checking, Tools, Verification of Concurrent Programs, Parametric Analysis, Program Analysis, and Hybrid Systems.

Table of contents :
Front Matter….Pages –
Hierarchical Set Decision Diagrams and Regular Models….Pages 1-15
Büchi Complementation and Size-Change Termination….Pages 16-30
Learning Minimal Separating DFA’s for Compositional Verification….Pages 31-45
RBAC-PAT: A Policy Analysis Tool for Role Based Access Control….Pages 46-49
ITPN-PerfBound: A Performance Bound Tool for Interval Time Petri Nets….Pages 50-53
Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches….Pages 54-57
Alpaga: A Tool for Solving Parity Games with Imperfect Information….Pages 58-61
Compositional Predicate Abstraction from Game Semantics….Pages 62-76
Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications….Pages 77-91
Computing Weakest Strategies for Safety Games of Imperfect Information….Pages 92-106
Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads….Pages 107-123
Semantic Reduction of Thread Interleavings in Concurrent Programs….Pages 124-138
Inferring Synchronization under Limited Observability….Pages 139-154
The Complexity of Predicting Atomicity Violations….Pages 155-169
MoonWalker : Verification of .NET Programs….Pages 170-173
Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays….Pages 174-177
The Yogi Project: Software Property Checking via Static Analysis and Testing….Pages 178-181
TaPAS: The Talence Presburger Arithmetic Suite….Pages 182-185
Transition-Based Directed Model Checking….Pages 186-200
Memoised Garbage Collection for Software Model Checking….Pages 201-214
Hierarchical Adaptive State Space Caching Based on Level Sampling….Pages 215-229
Static Analysis Techniques for Parameterised Boolean Equation Systems….Pages 230-245
Parametric Trace Slicing and Monitoring….Pages 246-261
From Tests to Proofs….Pages 262-276
Test Input Generation for Programs with Pointers….Pages 277-291
Specification Mining with Few False Positives….Pages 292-306
Path Feasibility Analysis for String-Manipulating Programs….Pages 307-321
Symbolic String Verification: Combining String Analysis and Size Analysis….Pages 322-336
Iterating Octagons….Pages 337-351
Verifying Reference Counting Implementations….Pages 352-367
Falsification of LTL Safety Properties in Hybrid Systems….Pages 368-382
Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints….Pages 383-397
All-Termination( T )….Pages 398-412
Ground Interpolation for the Theory of Equality….Pages 413-427
Satisfiability Procedures for Combination of Theories Sharing Integer Offsets….Pages 428-442
Bridging the Gap Between Model-Based Development and Model Checking….Pages 443-453
Back Matter….Pages –