Tools and Algorithms for the Construction and Analysis of Systems: 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proc

This book constitutes the refereed proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, held in Saarbrücken, Germany, March 26—April 3, 2011, as part of ETAPS 2011, the European Joint Conferences on Theory and Practice of Software. The 32 revised full papers presented were carefully reviewed and selected from 112 submissions. The papers are organized in topical sections on memory models and consistency, invariants and termination, timed and probabilistic systems, interpolations and SAT-solvers, learning, model checking, games and automata, verification, and probabilistic systems. Front Matter....Pages - Reliable Software Development: Analysis-Aware Design....Pages 1-2 Transition Invariants and Transition Predicate Abstraction for Program Termination....Pages 3-10 Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models....Pages 11-25 Compositionality Entails Sequentializability....Pages 26-40 Litmus : Running Tests against Hardware....Pages 41-44 Canonized Rewriting and Ground AC Completion Modulo Shostak Theories....Pages 45-59 Invariant Generation in Vampire....Pages 60-64 Enforcing Structural Invariants Using Dynamic Frames....Pages 65-80 Loop Summarization and Termination Analysis....Pages 81-95 Off-Line Test Selection with Test Purposes for Non-deterministic Timed Automata....Pages 96-111 Quantitative Multi-objective Verification for Probabilistic Systems....Pages 112-127 Efficient CTMC Model Checking of Linear Real-Time Objectives....Pages 128-142 Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic....Pages 143-157 Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems....Pages 158-172 Specification-Based Program Repair Using SAT....Pages 173-188 Optimal Base Encodings for Pseudo-Boolean Constraints....Pages 189-204 Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference....Pages 205-219 Next Generation LearnLib....Pages 220-223 Applying CEGAR to the Petri Net State Equation....Pages 224-238 Biased Model Checking Using Flows....Pages 239-253 S-TaLiRo : A Tool for Temporal Logic Falsification for Hybrid Systems....Pages 254-257 GAVS+: An Open Platform for the Research of Algorithmic Game Solving....Pages 258-261 Büchi Store: An Open Repository of Büchi Automata....Pages 262-266 QUASY: Quantitative Synthesis Tool....Pages 267-271 Unbeast: Symbolic Bounded Synthesis....Pages 272-275 Abstractions and Pattern Databases: The Quest for Succinctness and Accuracy....Pages 276-290 The ACL2 Sedan Theorem Proving System....Pages 291-295 On Probabilistic Parallel Programs with Process Creation and Synchronisation....Pages 296-310 Confluence Reduction for Probabilistic Systems....Pages 311-325 Model Repair for Probabilistic Systems....Pages 326-340 Boosting Lazy Abstraction for SystemC with Partial Order Reduction....Pages 341-356 Modelling and Verification of Web Services Business Activity Protocol....Pages 357-371 CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes....Pages 372-387 GameTime: A Toolkit for Timing Analysis of Software....Pages 388-392 Back Matter....Pages - This book constitutes the refereed proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, held in Saarbrucken, Germany, March 26-April 3, 2011, as part of ETAPS 2011, the European Joint Conferences on Theory and Practice of Software.