Tools and Algorithms for the Construction and Analysis of Systems
17th International Conference, TACAS 2011, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26--April 3, 2011, Proceedings
Published on 14. March 2011
XVI, 394 pages
978-3-642-19835-9 (ISBN)
Description
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.
More details
Other editions
Additional editions
Parosh Aziz Abdulla | K. Rustan M. Leino
Tools and Algorithms for the Construction and Analysis of Systems
17th International Conference, TACAS 2011, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26--April 3, 2011, Proceedings
Book
03/2011
1st Edition
Springer
€53.49
Shipment within 5-7 days
Content
- Title Page
- Foreword
- Preface
- Conference Organization
- Table of Contents
- Reliable Software Development: Analysis-Aware Design
- References
- Transition Invariants and Transition Predicate Abstraction for Program Termination
- Introduction
- Preliminaries
- Disjunctively Well-Founded Transition Invariants
- Transition Predicate Abstraction (TPA)
- Conclusion
- References
- Memory Models and Consistency
- Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models
- Introduction
- Preliminaries
- Programming Model
- Operational Memory Models
- Violations of Sequential Consistency
- Execution Traces
- Sequential Consistency and the Happens-Before Relation
- Monitoring Algorithms
- Comparison to SOBER
- Experimental Evaluation
- References
- Compositionality Entails Sequentializability
- Introduction
- A Compositional Abstract Semantics for Programs
- A High Level Overview of the Sequentialization
- Sequential and Concurrent Programs
- The Sequentialization
- Experience
- Future Directions
- References
- Litmus: Running Tests against Hardware
- Introduction
- High Level Overview
- Test Infrastructure and Parameters
- The Impact of Test Parameters
- References
- Invariants and Termination
- Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
- Introduction
- Ground AC-Completion
- Shostak Theories and Global Canonization
- Ground AC-Completion Modulo X
- Canonized Rewriting
- The AC(X) Algorithm
- Correctness
- Soundness
- Completeness
- Termination
- Experimental Results
- Conclusion and Future Works
- References
- Invariant Generation in Vampire
- Introduction
- Invariant Generation in Vampire: Overview
- Conclusion
- References
- Enforcing Structural Invariants Using Dynamic Frames
- Introduction
- Dynamic Frames
- Inferring Regions Automatically
- Verifiably Acyclic Data Structures
- A Characterization of $acyclicity$
- Preserving the Acyclicity Invariant
- Trees and Similar Data Structures
- Improving Precision
- Evaluation
- Related Work
- Conclusions
- References
- Loop Summarization and Termination Analysis
- Introduction
- Background
- Termination
- Loop Summarization
- Loop Summarization with Transition Invariants
- Selection of Candidate Invariants
- Evaluation
- Related Work
- Relation to Size-Change Termination Principle
- Relation to Other Research Using Transition Invariants
- Conclusion and Future Work
- References
- Timed and Probabilistic Systems
- Off-Line Test Selection with Test Purposes for Non-deterministic Timed Automata
- Introduction
- A Model of Open Timed Automata with Inputs/Outputs
- Open Timed Automata with Inputs/Outputs
- The Semantics of OTAIOs
- Properties and Operations
- Conformance Testing Theory
- The tioco Conformance Theory
- Refinement Preserving tioco
- Approximate Determinization Preserving tioco
- A Game Approach to Determinize Timed Automata
- Extensions to TAIOs and Adaptation to tioco
- Off-Line Test Case Generation
- Test Purposes
- Principle of Test Generation
- Conclusion
- References
- Quantitative Multi-objective Verification for Probabilistic Systems
- Introduction
- Background
- Probabilistic Automata (PAs)
- Verification of PAs
- Quantitative Multi-objective Verification
- Checking Multi-objective Queries
- Controller Synthesis
- Quantitative Assume-Guarantee Verification
- Conclusions
- References
- Efficient CTMC Model Checking of Linear Real-Time Objectives
- Introduction
- Preliminaries
- Continuous-Time Markov Chains
- Deterministic Timed Automata
- Decomposition for 1-Clock DTA
- Lumping
- Experimental Results
- Cyclic Polling Server
- Robot Navigation
- Systems Biology
- Parallelization
- Multi-clock DTA Objectives
- Conclusion
- References
- Interpolations and SAT-Solvers
- Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
- Motivations, Related Work and Goals
- Background: SMT(LA(Z))
- Generalities
- Efficient SMT(LA(Z)) Solving
- From LA(Z)-Solving to LA(Z)-Interpolation
- Interpolation for Diophantine Equations
- Interpolation for Inequalities
- Interpolation with Branch-and-Bound
- A Novel General Interpolation Technique for Inequalities
- Experimental Evaluation
- Description of the Benchmark Sets
- Comparison with the State-of-the-Art Tools Available
- Conclusions
- References
- Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems
- Introduction
- Stochastic Boolean Satisfiability
- Resolution for SSAT
- Interpolation for SSAT
- Generalized Craig Interpolants
- Computation of Generalized Craig Interpolants
- Interpolation-Based Probabilistic Model Checking
- Conclusion and Future Work
- References
- Specification-Based Program Repair Using SAT
- Introduction
- Basic Principle
- Our Framework
- Evaluation
- Candidates
- Metrics
- Results
- Discussion
- Correctness Argument
- Related Work
- Program Sketching Using SAT
- Program Repair Using Data Structure Repair
- Other Recent Work on Program Correction
- Conclusion
- References
- Optimal Base Encodings for Pseudo-Boolean Constraints
- Introduction
- Optimal Base Problems
- Encoding Pseudo-Boolean Constraints
- Measures of Optimality
- Optimal Base Search I: Heuristic Pruning
- Optimal Base Search II: Branch and Bound
- Optimal Base Search III: Search Modulo Product
- Experiments
- Related Work
- Conclusion
- References
- Learning
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- Introduction
- Preliminaries
- Inferring Loop Invariants with Algorithmic Learning
- Predicate Generation by Interpolation
- Initial Atomic Predicates
- Atomic Predicates from Incorrect Conjectures
- Atomic Predicates from Conflicting Abstract Counterexamples
- Algorithm
- Experimental Results
- tar from Tar
- parser from SPEC2000 Benchmarks
- Conclusions
- References
- Next Generation LearnLib
- Introduction
- Base Technology
- Modeling Learning Solutions
- Fast-Cycle Experimentation: The ZULU Experience
- Conclusion
- References
- Model Checking
- Applying CEGAR to the Petri Net State Equation
- Introduction
- The Reachability Problem
- Traversing the Solution Space
- Building Constraints
- Finding Partial Solutions
- Experimental Results
- Conclusion
- References
- Biased Model Checking Using Flows
- Introduction
- Applications to Distributed Message Passing Protocols
- Evaluation
- Related Work
- Preliminaries
- Biased BFS Algorithm
- Optimizations
- Biased DFS Algorithm
- Flows and Markings
- Experimental Evaluation
- Results
- Biased Procedures in Murphi
- Discussion
- Conclusion
- References
- S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems
- Introduction
- The S-TaLiRo Tool
- Usage
- Related Work
- References
- Games and Automata
- GAVS+: An Open Platform for the Research of Algorithmic Game Solving
- Introduction
- Supported Games in GAVS+
- Extension of Strips/PDDL for Game Solving: An Example
- References
- Büchi Store: An Open Repository of Büchi Automata
- Introduction
- Implementation and Main Features
- Use Cases
- References
- QUASY: Quantitative Synthesis Tool
- Introduction
- Synthesis from Combined Specifications
- Implementation Details
- Future Work
- References
- Unbeast: Symbolic Bounded Synthesis
- Introduction
- Tool Description
- Technology
- Experimental Results
- Conclusion
- References
- Verification (I)
- Abstractions and Pattern Databases: The Quest for Succinctness and Accuracy
- Introduction
- Preliminaries
- Notation
- Directed Model Checking
- Pattern Database Heuristics
- Pattern Selection Based on Downward Refinement
- Sufficiently Accurate Distance Heuristics
- Concretizable Traces and Safe Abstractions
- An Algorithm for Pattern Selection Based on Downward Refinement
- Related Work
- Evaluation
- Implementation Details
- Experimental Setup
- Experimental Results
- Directed Model Checking for Correct Systems?
- Conclusions
- References
- The ACL2 Sedan Theorem Proving System
- Introduction
- Termination Analysis Using Calling Context Graphs
- Random Testing and Proving: Synergistic Combination
- References
- Probabilistic Systems
- On Probabilistic Parallel Programs with Process Creation and Synchronisation
- Introduction
- Preliminaries
- Results
- Relationship with Probabilistic Pushdown Systems (pPDSs)
- Probability of Termination
- Probability of Finite Space
- Work and Time
- Case Studies
- Divide and Conquer
- Evaluation of Game Trees
- Conclusions and Future Work
- References
- Confluence Reduction for Probabilistic Systems
- Introduction
- Preliminaries
- Probability Theory and Probabilistic Automata
- Schedulers
- Branching Probabilistic Bisimulation
- Weak Steps for Probabilistic Automata
- Branching Probabilistic Bisimulation
- Confluence for Probabilistic Automata
- State Space Reduction Using Probabilistic Confluence
- Symbolic Detection of Probabilistic Confluence
- Case Study
- Conclusions
- References
- Model Repair for Probabilistic Systems
- Introduction
- Parametric Probabilistic Model Checking
- The Model Repair Problem
- The Max-Profit Model Repair Problem
- Model Repair as a Nonlinear Programming Problem
- Model Repair Feasibility and Optimality
- Model Repair and Optimal Control
- Applications
- Related Work
- Conclusions
- References
- Verification (II)
- Boosting Lazy Abstraction for SystemC with Partial Order Reduction
- Introduction
- Background
- The Problem of Multiple Interleavings
- Reduction Algorithms in ESST
- Partial-Order Reduction Techniques
- Applying POR to ESST
- Correctness of Reduction in ESST
- Related Work
- Experiments
- Conclusion and Future Work
- References
- Modelling and Verification of Web Services Business Activity Protocol
- Introduction
- WS-Business Activity Protocol
- Business Agreement with Coordination Completion
- Communication Policies
- Formal Modelling of BAwCC in UPPAAL
- Analysis of BAwCC
- Enhanced BAwCC
- Termination under Fairness
- Conclusion and Future Work
- References
- CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
- Introduction
- Architecture and Verification Technology
- Specification Languages
- Support for the LOTOS Language
- Support for the FSP Language
- Support for the LOTOS NT Language
- Support for Other Languages
- Model Checking
- Equivalence Checking
- Performance Evaluation
- Parallel and Distributed Methods
- Conclusion
- References
- GameTime: A Toolkit for Timing Analysis of Software
- Introduction
- Running Example
- The GameTime Approach
- Generating Basis Paths
- Sample Experimental Result
- References
- Author Index
