Tools and Algorithms for the Construction and Analysis of Systems

Name: Tools and Algorithms for the Construction and Analysis of Systems | 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 -- April 1, 2012, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 -- April 1, 2012, Proceedings

Cormac Flanagan Barbara König(Herausgeber*in)

Springer (Verlag)

1. Auflage

Erschienen am 22. März 2012

XIX, 560 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-28756-5 (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
Organization
Table of Contents
Invited Contribution
Quantitative Models for a Not So Dumb Grid
References
SAT and SMT Based Methods
History-Aware Data Structure Repair Using SAT
Introduction
Background
Cobbler Framework
Overview
Example
Implementation in Cobbler
Evaluation
EvaluationMetrics
Subject Programs
Errors
Subject Tools
Results
ANTLR BaseTree addChild
Related Work
Conclusions
References
The Guardol Language and Verification System
Introduction
An Example Guard
Generating Verification Conditions by Deduction
Guardol Operational Semantics
Decompilation
Verification Condition Solving Using SMT
Experimental Results
Discussion
References
A Bit Too Precise? Bounded Verification of Quantized Digital Filters
Introduction
Preliminaries: Digital Filter Basics
Bit-Precise Encoding
Real-Arithmetic Encoding
Experimental Evaluation
Related Work
Conclusion
References
Numeric Bounds Analysis with Conflict-Driven Learning
Introduction
Overview
Related Work
Program Model and Domain
Static Analysis as Second-Order Constraint Solving
Safety as Satisfiability
Conflict Driven Fixed Point Learning
Overview of CDFL
Data Structure and Phases of CDFL
Abstract Conflict Graphs
Implementation and Experiments
Conclusion
References
Automata
Ramsey-Based Analysis of Parity Automata
Introduction
Preliminaries
The Ramsey-Based Method for Parity Automata
Universality for NPA
Inclusion for NPA
Comparing Direct and Indirect Methods
Experimental Evaluation
A Random Model of Parity Automata
Comparison in Practice
Conclusion and Further Work
References
VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata
Introduction
Preliminaries
Design of the Library
Explicit Encoding
Semi-symbolic Encoding
Supported Operations
Removing Unreachable States
Downward and Upward Simulation
Simulation-Based Size Reduction
Bottom-Up Inclusion
Top-Down Inclusion
Computing Simulation over LTS
Experimental Evaluation of VATA
Experiments with the Explicit Encoding
Experiments with the Semi-symbolic Encoding
Conclusion
References
LTL to B¨uchi Automata Translation: Fast and More Deterministic
Introduction
Preliminaries
Alternating Formulae
Improvements in Reduction of LTL Formulae
Improvements in LTL to VWAA Translation
Improvements in VWAA to TGBA Translation
Optimization of BA
Implementation and Experimental Result
Conclusion
References
Model Checking
Pushdown Model Checking for Malware Detection
Introduction
Formal Model: Pushdown Systems
Malicious Behavior Specification
Environments, Predicates and Regular Expressions
Stack Computation Tree Predicate Logic
Modeling Malicious Behaviors Using SCTPL
SCTPL Model-Checking for Pushdown Systems
Variable Automata
Symbolic Alternating B¨uchi Pushdown Systems
From SCTPL Model Checking for PDSs to Emptiness of SABPDS
SCTPL Model-Checking for PDSs
Experiments
References
Aspect-Oriented Runtime Monitor Certification
Introduction
Related Work
Policy Language and Rewriter
Verifier
Case Studies
Conclusion and Future Work
References
Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems
Introduction
The Modal -Calculus
Networks of LTSs
Quotienting for Networks Using Networks
Formula Graph Simplifications
Simplification of Alternation-Free Formula Graphs
Implementation
Experimentation
Conclusion
References
From Under-Approximations to Over-Approximations and Back
Introduction
Overview
Abstract Reachability Graphs
The UFO Algorithm
Refinement
Implementation and Evaluation
Related Work
Conclusion
References
Case Studies
Automated Analysis of AODV Using UPPAAL
Introduction
Ad Hoc On-Demand Distance Vector Routing Protocol
The Basic Routine
Process Algebraic Model of AODV
Modelling AODV in UPPAAL
UPPAAL Automata
From AWN to UPPAAL
Experiments
Scenarios and Topologies
Properties
Modifications
Experimental Results
Related Work
Conclusions and Outlook
References
Modeling and Verification of a Dual Chamber Implantable Pacemaker
Introduction
Heart and Pacemaker Basics
System Modeling
Timed Automata and UPPAAL
System Overview
Basic DDD Pacemaker Modeling
Random Heart Model (RHM)
Verification Regarding Unsafe Regions
Lower Rate Limit
Upper Rate Limit
Verification Regarding Unsafe Transitions
Verification Procedure
Verification of the Mode-Switch Algorithm
Verification of Endless Loop Tachycardia (ELT) algorithm
Related Work
Conclusion and Future Work
References
Memory Models and Termination
Counter-Example Guided Fence Insertion under TSO
Introduction
Preliminaries
TSO Semantics
Single-Buffer Semantics
The SB Reachability Algorithm
Fence Insertion
Experimental Results
Conclusion
References
Java Memory Model-Aware Model Checking
Introduction
Background
Java PathRelaxer (JPR)
Properties of the JPR Algorithm
Experience
Related Work
Conclusion
References
Compositional Termination Proofsfor Multi-threaded Programs
Introduction
Preliminaries
Proof Rules
Compositional Termination of Multi-threaded Programs
Compositional Thread Termination
Proof Rule Automation
Experiments
Related Work
References
Deciding Conditional Termination
Introduction
Related Work
Preconditions for Non-termination
Difference Bounds Relations
Octagonal Relations
On the Existence of Linear Ranking Functions
Linear Affine Relations
Experimental Evaluation
Conclusions
References
Internet Protocol Verification
The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures
Introduction
The AVANTSSAR Platform
Description and Architecture
The Specification Languages ASLan and ASLan++
The Connectors Layer
The Orchestrator
The Validator
The AVANTSSAR Platform: Web Services and Web Interface
AVANTSSAR Library and Experimental Results
Technology Migration
Concluding Remarks
References
Reduction-Based Formal Analysis of BGP Instances
Introduction
Analyzing BGP Anomalies
Network Reduction
Hierarchical Reduction
Network Reduction
Examples: Reducing eBGP and iBGP Instances
Correctness of Network Reduction
eBGP Correctness
iBGP correctness: Cyclic iBGP Route Preference
iBGP Correctness: IGP-iBGP Consistency Property
Network Reduction in Maude
Computing the Static BGP Representation
Reduction by Merging All Pairs of Unifiable Nodes
Evaluation
Conclusion
References
Stochastic Model Checking
Minimal Critical Subsystems for Discrete-Time Markov Models
Introduction
Foundations
Computing Minimal Critical Subsystems for DTMCs
Formulation as an SMT Problem
Formulation as a Mixed Integer Linear Program
Optimizations
Computing Minimal Critical Subsystems for MDPs
SMT Formulation
MILP Formulation
Experimental Evaluation
Conclusion
References
Automatic Verification of Competitive Stochastic Systems
Introduction
Preliminaries
Property Specification: The Logic rPATL
Model Checking for rPATL
Computing Probabilities
Computing Rewards
Implementation and Case Studies
Experimental Results
MDSM: Microgrid Demand-Side Management
CDMSN: Collective Decision Making for Sensor Networks
Conclusions
References
Coupling and Importance Sampling for Statistical Model Checking
Introduction
Motivation and State of the Art
General Approach
Preliminaries
An Importance Sampling Method with Variance Reduction and Confidence Interval
Generalisation
Experimentation
Implementation
Example 1: Global Overflow in Tandem Queues
Example 2 : Parallel Random Walk
Example 3: Local Overflow in Tandem Queues
Example 4: Bottleneck in Tandem Queues
Conclusion
References
Verifying pCTL Model Checking
Introduction
Related Work
Foundations
Isabelle/HOL
Probability Space
Markov Chains
Verifying pCTL Model Checking
pCTL Formulas
Verifying the Algorithm
Discussion
Conclusion
References
Synthesis
Parameterized Synthesis
Introduction
Preliminaries
Parameterized Synthesis
Definition
Reduction of Parameterized to Isomorphic Synthesis
Decidability
Bounded Isomorphic Synthesis
Bounded Synthesis
Adaption to Token Rings
Synthesizing a Parameterized Arbiter
A Framework for Parameterized Synthesis
General Token-Passing Systems
Other Results with Cutoffs
Conclusions
References
QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification
Introduction
Architecture of QuteRTL Framework
Overview of QuteRTL Framework
Supported Features of QuteRTL
Comparison with other Open Source RTL Front-End
Tool Implementation
Parser and Preprocessor
RTL Synthesis and Circuit Flattening
Applications of QuteRTL
Intent Extraction
Model Checking
Availability for General Users
A Brief Description to QuteRTL Command-Line Interface
Example: RTL to Gate Synthesis Flow
Example: Hierarchical Word-Level Netlist Creation
Example: Property Checking
Conclusion
References
Template-Based Controller Synthesis for Timed Systems
Introduction
Timed Systems
Template-Based Controller Synthesis
Symbolic Parameter Synthesis
Precise Computation of the Feasible Instantiations
The Focus Abstraction
Abstraction Refinement
Experimental Results
Conclusion
References
Provers and Analysis Techniques
Zeno: An Automated Prover for Properties of Recursive Data Structures
Introduction
Zeno's Internal Functional Language HC
Proof Steps
Heuristics
Prioritize (eql) and (con), and Counterexamples
Applying (cut) Only When (case) is also Possible
Critical Terms
Critical Paths
Comparisons and the Output of Isabelle Proofs
Conclusions and Future Work
References
A Proof Assistant for Alloy Specifications
Introduction
Related Work
Background
Alloy and the Alloy Analyzer
The KeY Proof System
Axiomatization of Alloy0
Declarations
Relational Expressions
Integer Expressions and Cardinality
Formulas
The Ordering Module
Theoretical Properties
Reasoning Strategy
Evaluation
Automation
Interactive Proofs
Conclusion
References
Reachability under Contextual Locking
Introduction
Model
Multi-pushdown Systems
Contextual Locking
Pairwise Reachability
Well-Bracketed Computations
Algorithm for Deciding the Pairwise Reachability
Conclusions
References
Bounded Phase Analysis of Message-Passing Programs
Introduction
Asynchronous Message-Passing Programs
Program Syntax
Single-Processor Semantics
Multi-processor Semantics
Phase-Bounded Execution
Phase-Bounding for Single-Processor Programs
Phase-Bounding for Multi-processor Programs
Related Work
Conclusion
References
Tool Demonstrations
Demonstrating Learning of Register Automata
Introduction
Active Automata Learning
Register Automata
The Tool Demo
Conclusion
References
Symbolic Automata: The Toolkit
Bek
UTF8Encode Example
Bek on Rise4Fun.com
Rex on Rise4Fun.com
McScM: A General Framework for the Verification of Communicating Machines
Introduction
Safety Verification of Communicating Machines
A Closer Look on verify's Modular Architecture
A Comparative Benchmark of Verification Algorithms
The McScM Framework
References
SLMC: A Tool for Model Checking Concurrent Systemsag ainst Dynamical Spatial Logic Specifications
Introduction
Checking a Topological Property of a Distributed Protocol
Verification Algorithms and Implementation
Concluding Remarks
References
TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets
Introduction
Tool Description
Experiments
Conclusion
References
A Platform for High Performance Statistical Model Checking - PLASMA
Introduction
Software Architecture
Stochastic Simulation Algorithm
Rare Properties and Importance Sampling
Results
Conclusion and Future Challenges
References
Competition on Software Verification
Competition on Software Verification
Introduction
Procedure and Schedule
Definitions and Rules
Benchmark Verification Tasks
Participating Teams
Results and Discussion
Summary and Future Plans
References
Predicate Analysis with BLAST 2.7
Verification Approach
Tool Architecture
Tool Improvements and Benchmarking
Downloading and Using BLAST
References
CPAchecker with Adjustable Predicate Analysis
Verification Approach
Software Architecture
Strengths and Weaknesses
Setup and Configuration
Project and Contributors
References
Block Abstraction Memoization for CPAchecker
Verification Approach
Implementation
Installation Instructions
References
Context-Bounded Model Checking with ESBMC 1.17
Overview
Verification Approach
Architecture, Implementation, and Availability
Results
References
Proving Reachabili ty Using FShell
Overview
Architecture
Strengths and Weaknesses
Tool Setup
References
LLBMC: A Bounded Model Checker for LLVM's Intermediate Represent ation
Verification Approach
Software Architecture
Strengths and Weaknesses of the Approach
Tool Setup and Configuration
References
Predator: A Verification Tool for Programs with Dynamic Linked Data Structures
Introduction
Overview of Predator
Experience with Predator
Conclusions and Future Work
Reference
HSF(C): A Software Verifier Based on Horn Clauses
Verification Approach
Software Architecture
Discussion
Tool Setup
References
SatAbs: A Bit-Precise Verifier for C Programs
Verification Approach
Architecture
Strengths and Weaknesses
Tool Setup
References
Wolverine: Battling Bugs with Interpolants
Approach
Software Architecture
Tool Setup and Usage
Strengths and Limitations
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken