Tools and Algorithms for the Construction and Analysis of Systems

Model Checking I.- Hierarchical Set Decision Diagrams and Regular Models.- Büchi Complementation and Size-Change Termination.- Learning Minimal Separating DFA's for Compositional Verification.- Tools I.- RBAC-PAT: A Policy Analysis Tool for Role Based Access Control.- ITPN-PerfBound: A Performance Bound Tool for Interval Time Petri Nets.- Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches.- Alpaga: A Tool for Solving Parity Games with Imperfect Information.- Game-Theoretic Approaches.- Compositional Predicate Abstraction from Game Semantics.- Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications.- Computing Weakest Strategies for Safety Games of Imperfect Information.- Verification of Concurrent Programs.- Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads.- Semantic Reduction of Thread Interleavings in Concurrent Programs.- Inferring Synchronization under Limited Observability.- The Complexity of Predicting Atomicity Violations.- Tools II.- MoonWalker: Verification of .NET Programs.- Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays.- The Yogi Project: Software Property Checking via Static Analysis and Testing.- TaPAS: The Talence Presburger Arithmetic Suite.- Model Checking II.- Transition-Based Directed Model Checking.- Memoised Garbage Collection for Software Model Checking.- Hierarchical Adaptive State Space Caching Based on Level Sampling.- Parametric Analysis.- Static Analysis Techniques for Parameterised Boolean Equation Systems.- Parametric Trace Slicing and Monitoring.- Generative Approaches.- From Tests to Proofs.- Test Input Generation for Programs with Pointers.- Specification Mining with Few False Positives.- Program Analysis.- Path Feasibility Analysis forString-Manipulating Programs.- Symbolic String Verification: Combining String Analysis and Size Analysis.- Iterating Octagons.- Verifying Reference Counting Implementations.- Hybrid Systems.- Falsification of LTL Safety Properties in Hybrid Systems.- Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints.- Decision Procedures and Theorem Proving.- All-Termination(T).- Ground Interpolation for the Theory of Equality.- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets.- Invited Contribution.- Bridging the Gap Between Model-Based Development and Model Checking.