Tools and Algorithms for the Construction and Analysis of Systems: 17th International Conference, Tacas 2011

by Adbulla, Parosh Aziz; Leino, K, Rustan M.

• ISBN13: 9783642198342
• ISBN10: 3642198341
• Format: Paperback
• Copyright: 2011-07-25
• Publisher: Springer-Verlag New York Inc

Summary

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#xC3;#xBC;cken, Germany, March 26#xE2;#xAC;#x1D;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.

Table of Contents

Reliable Software Development: Analysis-Aware Design (Invited Talk)	p. 1
Transition Invariants and Transition Predicate Abstraction for Program Termination (Invited Talk)	p. 3
Memory Models and Consistency
Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models	p. 11
Compositionality Entails Sequentializability	p. 26
Litmus: Running Tests against Hardware	p. 41
Invariants and Termination
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories	p. 45
Invariant Generation in Vampire	p. 60
Enforcing Structural Invariants Using Dynamic Frames	p. 65
Loop Summarization and Termination Analysis	p. 81
Timed and Probabilistic Systems
Off-Line Test Selection with Test Purposes for Non-deterministic Timed Automata	p. 96
Quantitative Multi-objective Verification for Probabilistic Systems	p. 112
Efficient CTMC Model Checking of Linear Real-Time Objectives	p. 128
Interpolations and SAT-Solvers
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic	p. 143
Generailized Craig Interpolation for Stochastic Boolean Satisfiability Problems	p. 158
Specification-Based Program Repair Using SAT	p. 173
Optimal Base Encodings for Pseudo-Boolean Constraints	p. 189
Learning
Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference	p. 205
Next Generation LearnLib	p. 220
Model Checking
Applying CEGAR to the Petri Net State Equation	p. 224
Biased Model Checking Using Flows	p. 239
S-TALIRO: A Tool for Temporal Logic Falsification for Hybrid Systems	p. 254
Games and Automata
GAVS+: An Open Platform for the Research of Algorithmic Game Solving	p. 258
Büchi Store; An Open Repository of Büchi Automata	p. 262
QUASY: Quantitative Synthesis Tool	p. 267
Unbeast: Symbolic Bounded Synthesis	p. 272
Verification (I)
Abstractions and Pattern Databases: The Quest for Succinctness and Accuracy	p. 276
The ACL2 Sedan Theorem Proving System	p. 291
Probabilistic Systems
On Probabilistic Parallel Programs with Process Creation and Synchronisation	p. 296
Confluence Reduction for Probabilistic Systems	p. 311
Model Repair for Probabilistic Systems	p. 326
Verification (II)
Boosting Lazy Abstraction for SystemC with Partial Order Reduction	p. 341
Modelling and Verification of Web Services Business Activity Protocol	p. 357
CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes	p. 372
GameTime: A Toolkit for Timing Analysis of Software	p. 388
Author Index	p. 393
Table of Contents provided by Ingram. All Rights Reserved.