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

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 -