Tools and Algorithms for the Construction and Analysis of Systems

Name: 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
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

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

Parosh Aziz Abdulla K. Rustan M. Leino(Herausgeber*in)

Springer (Verlag)

Erschienen am 14. März 2011

XVI, 394 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-19835-9 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken