Automated Technology for Verification and Analysis
9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011, Proceedings
Published on 1. October 2011
XIV, 532 pages
978-3-642-24372-1 (ISBN)
Description
This book constitutes the refereed proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011, held in Taipei, Taiwan, in October 2011.
The 23 revised regular papers presented together with 5 invited papers, 11 short papers, and 2 tool papers, were carefully reviewed and selected from 75 submissions. The papers address all theoretical and practical aspects of automated analysis, verification and synthesis; thus providing a forum for interaction between the regional and the international research communities and industry in the field.
The 23 revised regular papers presented together with 5 invited papers, 11 short papers, and 2 tool papers, were carefully reviewed and selected from 75 submissions. The papers address all theoretical and practical aspects of automated analysis, verification and synthesis; thus providing a forum for interaction between the regional and the international research communities and industry in the field.
More details
Other editions
Additional editions
Tevfik Bultan | Pao-Ann Hsiung
Automated Technology for Verification and Analysis
9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011, Proceedings
Book
09/2011
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Invited Papers
- Statistical Model Checking for Cyber-Physical Systems
- Introduction
- Background
- Statistical Model Checking
- The Monte Carlo Method
- Importance Sampling
- Basics
- The Cross-Entropy Method
- Experiments
- Conclusions
- References
- Max and Sum Semantics for Alternating Weighted Automata
- Introduction
- Alternating Weighted Automata
- The Max Semantics
- The Duality between the Min and the Max Semantics
- Expressive Power
- Arithmetics
- The Sum Semantics
- Exponential Weights
- Expressive Power
- sum-UWA and Polynomials
- Discussion
- References
- Making Software Verification Tools Really Work
- Introduction
- Community Support for Tool Development
- Allocating Resources to Tool Development
- The Need for Robust Tools
- Program Semantics: Minimum Requirements
- What Should All Software Verification Tools Handle, a minima?
- The Challenges of Semantic Features in Real-World Languages
- The Lack of Guidance in the Process of Writing Tools
- Proposals for Supporting the Development of Software Verification Tools
- Publication Incentives
- Benefits from Building Tools
- Standards for Tool Interfaces
- Benchmarks to Drive Quality, Comparability, and Competition
- Summary
- References
- Synthesizing, Verifying, and Debugging SoC with FSM-Based Specification of On-Chip Communication Protocols
- Introduction
- FSM-Based Specification of On-Chip Communication Protocols
- Automatic Generation of On-Chip Communication Protocol Converters
- Post-Silicon Verification and Debugging of SoC with FSM-Based Specifications of On-Chip Communication Protocols
- Concluding Remarks
- References
- Automated Analysis of Industrial Embedded Software
- Introduction
- Unified Storage Platform for OneNAND Flash Memory
- Overview of the Unified Storage Platform
- Logical-to-Physical Sector Translation
- Analysis Results and Discussions
- Concolic Testing Technique
- Samsung Linux Platform (SLP) for Smartphones
- File Manager
- Security Library
- Conclusion and Future Work
- References
- Regular Papers
- Nondeterministic Update of CTL Models by Preserving Satisfaction through Protections
- Introduction
- Technical Preliminaries
- CTL Update Algorithms
- Nondeterministic Pseudo-Code
- Modification of Models
- A Direct Update Algorithm for -XCTL
- An Algorithm for Updating Protected Models
- Model Update for -CTL and Addition of States
- Soundness and Completeness of XUpdprot
- Synthesizing a Model of the Mutual Exclusion Problem
- Related Work and Conclusions
- References
- Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols
- Introduction
- Processes
- Type System
- Basic Ideas
- Types
- Typing
- Type Inference
- Implementation and Experiments
- Extensions
- Related Work
- References
- Formalization of Finite-State Discrete-Time Markov Chains in HOL
- Introduction
- Related Work
- Probability Theory and Random Variables in HOL
- Formal Modeling of Discrete-Time Markov Chains
- Verification of Discrete-Time Markov Chain Properties
- Joint Probability of a Markov Chain
- Chapman-Kolmogorov Equation
- Absolute Probabilities
- Steady State Probabilities
- Generalized Stationary Distribution
- Application: Binary Communication Channel
- Conclusions
- References
- An Alternative Definition for Timed Automata Composition
- Introduction
- Related Work
- A New Composition of Timed Automata
- Differences with Existing Approaches
- Benefits of the Proposal
- Transformation to Basic Uppaal
- Transition System Extensions
- Labelled Transition Systems
- Composable Labelled Transition Systems
- Product of Composable Labelled Transition Systems
- CLTS with Location Invariants
- Timed Transition Systems Extensions
- ETTS Timed Traces
- Networks of Timed Automata
- Timed Automata
- Semantics of Timed Automata
- Networks of Timed Automata
- Semantics of a NTA
- Composition and Refinement
- Conclusion
- References
- Model Checking EGF on Basic Parallel Processes
- Introduction
- Preliminaries
- Model Checking the Logic EGF
- Fixed Formula
- Conclusion
- References
- Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited
- Introduction
- Preliminaries
- Mean-Payoff Parity Games
- Mean-Penalty Parity Games
- Conclusion
- References
- Algorithms for Synthesizing Priorities in Component-Based Systems
- Introduction
- Component-Based Modeling and Priority Synthesis
- Behavioral-Interaction-Priority Framework
- Priority Synthesis for Safety and Deadlock Freedom
- A Framework of Priority Synthesis Based on Fault-Localization and Fault-Repair
- System Encoding
- Step A. Finding Fix Candidates Using Fault-Localization
- Step B. Priority Synthesis via Conflict Resolution - From Stateful to Stateless
- Optimization
- Handling Complexities
- Data Abstraction
- Alphabet Abstraction
- Assume-Guarantee Based Priority Synthesis
- Evaluation
- Related Work
- Conclusion
- References
- Trust Metrics for the SPKI/SDSI Authorisation Framework
- Introduction
- Formal Definitions
- Complexity of Computing the Trust Metrics
- Approximation of the Trust Metrics
- Spookey and Experimental Results
- Future Work
- References
- Antichain-Based QBF Solving
- Introduction
- Preliminaries
- Notations and QBF Problem
- QBF Problem as a Game
- Structure in the And-Or Graph and Antichains
- Algorithms
- Maximal and Minimal Valuations
- Antichain-Based Algorithm
- Certificates
- Optimizations
- Guiding the Search to Promising Valuations
- Improving the Information about Losing and Winning Nodes
- Experimental Results
- Conclusion and Perspectives
- References
- A Hierarchical Approach for the Synthesis of Stabilizing Controllers for Hybrid Systems
- Introduction
- Controller Synthesis for Stabilization Games
- Stabilization Games
- Algorithm for Stabilization Games
- Nonlinear Systems and Discretizations
- Nonlinear Systems with Inputs
- Discretizations
- Hierarchical Approach to Controller Synthesis
- Abstractions Preserving Controllability
- Hierarchical Abstractions in ODE Systems
- Experiments
- Conclusions and Future Work
- References
- Formal Analysis of Online Algorithms
- Introduction
- Preliminaries
- Weighted Automata
- Online Algorithms
- An Automata-Theoretic Approach to Reasoning about Online Algorithms
- Adding Assumptions on the Environment
- Reasoning about Online Algorithms with Look-Ahead
- Symbolic Model-Checking Algorithm
- References
- Modal Transition Systems: Composition and LTL Model Checking
- Introduction
- Preliminaries
- LTL Model Checking
- Parallel Composition
- Common Implementation Problem and Conjunction
- Conclusion and Future Work
- References
- Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata
- Introduction
- Preliminaries
- Downward Inclusion Checking
- Basic Algorithm of Downward Inclusion Checking
- Optimized Algorithm of Downward Inclusion Checking
- Experimental Results
- Semi-symbolic Representation of Tree Automata
- Binary Decision Diagrams
- Encoding the Transition Function of a TA Using Shared MTBDDs
- Downward Simulation on Semi-symbolically Encoded TA
- Downward Inclusion Checking on Semi-symbolically Encoded TA
- Experimental Results
- Conclusion
- References
- Assembling Sessions
- Introduction
- Motivational Example
- Session Systems
- Preliminaries
- Session Schemes
- Sessions
- Agents
- Scheduling
- Semantics of Session Systems
- Conclusion
- References
- Parametric Modal Transition Systems
- Introduction
- Parametric Modal Transition Systems
- Motivation
- Definition of Parametric Modal Transition System
- Modal Refinement
- Complexity of Modal Refinement Checking
- Parameter-Free Systems
- Systems with Parameters
- Conclusion and Future Work
- References
- Policy Iteration within Logico-Numerical Abstract Domains
- Introduction
- Abstract Interpretation and Abstract Domains
- Abstract Equation Solving and Policy Iteration
- Integrating Policies in Numerical Abstract Domains
- Policy for Logico-Numerical Abstract Domain
- Experiments
- Conclusion
- References
- Small Strategies for Safety Games
- Introduction
- Safety Games and Strategies
- Learning Small Strategies
- A Teacher for Strategy Automata
- An Improved Learning Algorithm
- Main Result
- Experiments
- Conclusion
- References
- Multi-core Nested Depth-First Search
- Introduction
- Background (LTL Model Checking)
- Related Work
- Multi-core Ndfs
- A Basic Multi-core Swarmed Ndfs
- Multi-core Ndfs with Global Coloring
- Correctness Proof
- Extensions
- Experiments
- Models with Accepting Cycles
- Models without Accepting Cycles
- Conclusions
- References
- Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking
- Introduction
- Preliminaries
- Boolean Formulas
- TGBA
- Kripke Structure
- Self-Loop Aggregation Product (SLAP)
- Definition
- Proof of Correctness
- Mixing SLAP and Fully Symbolic Approaches
- Experimentations
- Implementation
- Benchmark
- Conclusion and Perspectives
- References
- A Lightweight Approach for Loop Summarization
- Introduction
- Inferring Summary Constraints
- Cycle Exit Information
- Inter Variable Relations
- Quantified Array Formulas
- Function Infer
- Cycle Elimination
- Divergence (Cycle) Detection
- Cycle Replacement
- Extended CEGAR
- Integrating Loop Summarization into CEGAR
- Experimental Evaluation
- Related Work
- Conclusion
- References
- A Succinct Canonical Register Automaton Model
- Introduction
- Data Languages and Register Automata
- Symbolic Representation of Data Languages
- Nerode Congruence and Canonical Form
- Comparison between Different Automata Models
- Conclusions and Future Work
- References
- Parallel Nested Depth-First Searches for LTL Model Checking
- Introduction
- Background
- The LTL Model Checking Problem
- Algorithms Based on Nested Depth-First Search
- Parallel Algorithms for LTL Model Checking
- mc-ndfs, a Multi-core Algorithm for LTL Model Checking
- Difficulty of Parallelising ndfs
- Principle of the Algorithm
- Details of the Algorithm
- Proof of the Algorithm
- Complexity of the Algorithm
- Using Tarjan's Algorithm in Nested Searches
- Experimental Results
- Conclusion and Perspectives
- References
- Evaluating LTL Satisfiability Solvers
- Introduction
- Preliminaries
- Solvers
- Benchmarks
- Methodology
- Results
- Potential of a Portfolio Solver
- Conclusion
- References
- Tool Papers
- McAiT - A Timing Analyzer for Multicore Real-Time Software
- Introduction
- Main Features and Implementation of McAiT
- References
- MIO Workbench: A Tool for Compositional Design with Modal Input/Output Interfaces
- Context
- Tool Architecture
- Experiments and Future Work
- References
- Short Papers
- The Buck Stops Here: Order, Chance, and Coordination in Distributed Control
- Introduction
- Knowledge Based Control in a Nutshell
- Reducing Process Hanging and Passing Responsibility
- Refinig Knowledge
- References
- Symbolic Verification and Test Generation for a Network of Communicating FSMs
- Introduction
- Preliminaries
- Decision Diagrams
- Previous Work
- System Framework and Symbolic Encoding
- Symbolic NCFSM Verification
- Symbolic NCFSM Test Derivation
- Experimental Results
- Conclusion
- References
- Hierarchical Counterexamples for Discrete-Time Markov Chains
- Introduction
- Preliminaries
- SCC-Based Model Checking
- Counterexample Generation
- The Basic Hierarchical Algorithm
- Search Algorithms
- Experimental Results
- References
- Efficient Loop Navigation for Symbolic Execution
- Introduction
- Overview
- The Algorithm
- Experimental Results
- Related Work
- References
- An Efficient Algorithm for Learning Event-Recording Automata
- Introduction
- Preliminaries
- Timed Languages and Event-Recording Automata
- The L* Algorithm
- An Efficient Algorithm for Learning ERA
- The TL* Algorithm
- Analysis of the TL* Algorithm
- Conclusion and Future Work
- References
- Discretizing Affine Hybrid Automata with Uncertainty
- Introduction
- Affine Hybrid Automata with Uncertainty
- From Affine Hybrid Automata to Affine Programs
- Conclusion
- References
- What's Decidable about Weighted Automata?
- Introduction
- Preliminaries
- Weighted Automata with Integer Weights
- Weighted Automata with Positive Weights
- Universality Is PSPACE-Complete
- Containment Is Undecidable
- References
- Widening with Thresholds for Programs with Complex Control Graphs
- Introduction and Related Work
- The Widening/Narrowing Approach in Practice
- Inferring Thresholds by Propagating Disjunctions
- Experiments and Conclusion
- References
- Linear Hybrid System Falsification through Local Search
- Introduction
- Problem Formulation
- Descent in the Robustness Ellipsoid
- Experiments
- Conclusions
- References
- Learning-Based Compositional Verification for Synchronous Probabilistic Systems
- Introduction
- Preliminaries
- Assume-Guarantee for Synchronous Probabilistic Systems
- Deciding Language Inclusion for PFAs
- L*-Style Learning for PFAs
- Learning Assumptions for Compositional Verification
- Implementation and Results
- References
- An Algorithmic Framework for Synthesis of Concurrent Programs
- Introduction
- Algorithmic Framework
- Correctness of Synthesis
- Extensions and Experiments
- Concluding Remarks
- References
- Author Index
