Computer Aided Verification

Name: Computer Aided Verification | 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings

Madhusudan Parthasarathy Sanjit A. Seshia(Herausgeber*in)

Springer (Verlag)

1. Auflage

Erschienen am 22. Juni 2012

XVI, 789 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-31424-7 (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
Preface
Organization
Table of Contents
Invited Talks
Synthesis and Some of Its Challenges
Model Checking Cell Biology
Invited Tutorials
Synthesizing Programs with Constraint Solvers
IC3 and beyond: Incremental, Inductive Verification
References
Formal Verification of Genetic Circuits
References
From C to Infinity and Back: Unbounded Auto-active Verification with VCC
References
Automata and Synthesis
Deterministic Automata for the (F,G)-Fragment of LTL
Introduction
Linear Temporal Logic
Deterministic Automaton for the (F,G)-Fragment
Muller Acceptance Condition
Correctness
Generalized Rabin Condition
Rabin Condition
Complexity
Experimental Results and Evaluation
Discussion on Extensions
Conclusions
References
Efficient Controller Synthesis for Consumption Games with Multiple Resource Types
Introduction
Definitions
Algorithms for General Consumption Games
Algorithms for One-Player and Decreasing Consumption Games
The Emptiness and Membership Problems
Minimal Safe Configurations and Multi-distance Reachability
Computing Safe(s) in One-Player Consumption Games
Computing Safe(s) in Decreasing Consumption Games
Conclusions
References
ACTL n LTL Synthesis
Introduction
Preliminaries
Translating LTL Formulas into UVWs
The Case of Automata over Infinite Words
Decomposing a Language over Finite Words into a Non-deterministic Very-Weak Automaton
Reduction of the Synthesis Problem to Parity Games
Solving Parity Games Symbolically
Experimental Results
Conclusion
References
Inductive Inference and Termination
Learning Boolean Functions Incrementally
Introduction
Preliminary
The CDNF Algorithm
Incremental Learning
Incremental Teacher
The CDNF+ Algorithm
The CDNF++ Algorithm
Experiments
Conclusion
References
Interpolants as Classifiers
Introduction
An Overview of the Technique
Preliminaries
SVM Primer
Classification Based Algorithms for Interpolation
Algorithm for Intersection of Half-spaces
A Sound Algorithm
Handling Superficial Non-linearities
Experiments
Related Work
Conclusion
References
Termination Analysis with Algorithmic Learning
Introduction
Termination Analysis via Transition Invariants
Program Termination and Transition Invariant
Intensional Transition Invariants
Algorithmic-Learning-Based Inference of Transition Invariants
CDNF Learning Algorithm
Learning Algorithm as an Inference Engine
Algorithms for Mechanical Teacher
Experiments
Related Work
Conclusion
References
Automated Termination Proofs for Java Programs with Cyclic Data
Introduction
Handling Irrelevant Cycles
Abstract States in Termination Graphs
Constructing the Termination Graph
Proving Termination via Term Rewriting
Handling Marking Algorithms on Cyclic Data
Constructing the Termination Graph
Proving Termination of Marking Algorithms
Handling Algorithms with Definite Cyclicity
Constructing the Termination Graph
Proving Termination of Algorithms with Definite Reachability
Experiments and Conclusion
References
Proving Termination of Probabilistic Programs Using Patterns
Introduction
Preliminaries
Probabilistic Programs
Patterns
Nondeterministic Programs
Our Algorithm
Implementing Pattern Checkers
Experimental Evaluation
Conclusions
References
Abstraction
The Gauge Domain: Scalable Analysis of Linear Inequality Invariants
Introduction
The Gauge Abstraction
Abstract Interpretation Framework
The Gauge Domain
Experimental Evaluation
Conclusion
References
Diagnosing Abstraction Failure for Separation Logic-Based Analyses
Introduction
Separation Logic-Based Shape Analysis
Abstraction Failure Diagnosis
Feasibility Checking
A Memory Model
Encoding to SMT
Doomed State Synthesis
Experimental Evaluation
Related Work
Conclusion
References
A Method for Symbolic Computation of Abstract Operations
Introduction
Overview
Algorithm for Assume"0365ssume[](A)
Instantiations
Experiments
Applications to Other Symbolic Operations
Related Work
References
Leveraging Interpolant Strength in Model Checking
Introduction
Preliminaries
Craig Interpolation
Resolution Proofs
Strength of Interpolants
Simultaneous Abstraction with Interpolation
Problem Description
Proof for Pudlák's System
Proof Generalization
Application to Model Checking
Inductive Sequence of Interpolants
Problem Description
Proof for Pudlák's System
Proof Generalization
Application to Model Checking
Related Work
Conclusion
References
Concurrency and Software Verification
Detecting Fair Non-termination in Multithreaded Programs
Introduction
Recursive Multithreaded Programs
Bounded Compositional Non-termination Analysis
Annotated Traces
Compositional Detection of Periodic Traces
From Thread-Periodic Traces to Sequential Reachability
Encoding Fairness
Reduction to Sequential Program Analysis
Experimental Evaluation
Related Work
Conclusion
References
Lock Removal for Concurrent Trace Programs
Introduction
Motivation
Lock Removal: The Core Idea
The Lock Removal Strategy
Conservative Static Check
Compositional Lock Removal
Deciding Static Reachability
Compositional Analysis
Identifying the Locks to Be Retained
Applying Lock Removal to the Running Example
Experiments
Related Work
Conclusions
References
How to Prove Algorithms Linearisable
Introduction
Example
Linearisability and Refinement
Proving Linearisability with Backward Simulation
Backward Simulation for the Case Study
Verification with KIV
Related Work
Conclusion and Future Work
References
Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters
Introduction
Model Definition
Synchronisation-Bounded Reachability
Comparison with Context-Bounded Model Checking
Optimisations
Implementation and Experimental Results
Conclusions and Future Work
References
Software Model Checking via IC3
Introduction
Background and Notation
IC3withSMT
Tree-Based IC3
HybridTreeIC3
Implementation and Experiments
Implementation Details
Benchmarks and Evaluation
Results
Related Work
Conclusions and Future Work
References
Biology and Probabilistic Systems
Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits
Introduction
Delayed CTMC
Genetic Regulatory Circuits
Specifying Genetic Regulatory Circuits
Dynamics in Terms of Delayed CTMCs
Comparison of Different Semantics for GRCs
Probability Distributions for Delayed Reactions
Examples Demonstrating Qualitatively Different Behavior
Behavior Computation of Delayed CTMC
Implementation and Results
Conclusion
References
Assume-Guarantee Abstraction Refinement for Probabilistic Systems
Introduction
Preliminaries
Counterexamples to Strong Simulation
CEGAR for Checking Strong Simulation
Assume-Guarantee Abstraction Refinement
Implementation and Results
Conclusion and Future Work
References
Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking
Introduction
Importance Sampling
Estimators
The Cross-Entropy Method
A Parametrised Cross-Entropy Algorithm
The Algorithm
Examples
Chemical Network
Repair Model
Conclusions and Future Work
References
Embedded and Control Systems
Timed Relational Abstractions for Sampled Data Control Systems
Introduction
Sampled Data Control Systems
Relationalization
Dealing with Autonomous Transitions
Experimental Evaluation
References
Approximately Bisimilar Symbolic Models for Digital Control Systems
Introduction
Systems and Approximate Equivalences
Symbolic Models for Control Systems
Main Construction
Comparison with Previous Techniques
Examples
DC Motor
Motion Planing
Pendulum with Resource Constraints
References
Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System
Introduction
The Application: Logica Di Sicurezza
The Radio Block Section
Verification Properties of the RBS
The Velos Specification
Verification Techniques and Tools
Verification Approach
From Velos Specifications to NuSMV Models
From Velos Specifications to C Programs
Model Checking Sequential Software with Multiple Assertions
Experimental Evaluation
Benchmarks
Setup and Configurations
Results of Experiments
Remarks on other Experiments
Related Work
Conclusions and Future Work
References
SAT/SMT Solving and SMT-based Verification
Minimum Satisfying Assignments for SMT
Introduction
Minimum Satisfying Assignments and Their Properties
A Branch-and-Bound Algorithm for Computing MSAs
Variable Order and Initial Cost Estimate
Using Implicants to Approximate MSAs
Computing Minimum T-satisfiable Monotone Implicants
Using Implicates to Identify Non-universal Sets
Implementation
Experimental Results
Other Strategies to Obtain Bound and Variable Order
Related Work
Conclusion
References
When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way
Introduction
Preliminaries
XOR Constraints
Resolution Refutation and Craig Interpolation
Satisfiability Solving under XOR Constraints
XOR Reasoning
Implementation Issues
Refutation and Interpolation
Interpolant Generation
Implementation Issues
Experimental Results
Related Work
Conclusions and Future Work
References
A Solver for Reachability Modulo Theories
Introduction
The Corral Architecture
Stratified Inlining
Variable Abstraction and Refinement
Hierarchical Refinement
Evaluation
Evaluating Components of Corral
SDV Benchmarks
SV-COMP Benchmarks
.NET Benchmarks
Related Work
References
Timed and Hybrid Systems
On Decidability of Prebisimulation for Timed Automata
Introduction
Timed Automata
Semantics
Bisimulations for Timed Systems
Timed Performance Prebisimulation
Zone Valuation Graph and Deciding Prebisimulation
Zone Valuation Graph
Decidability of Timed Performance Prebisimulation
Generating Zone Valuation Graph
Algorithm: Deciding Timed Performance Prebisimulation Using Zone Valuation Graph
Conclusion and Future Work
References
Exercises in Nonstandard Static Analysis of Hybrid Systems
Introduction
Preliminaries
A Leading Example: ETCS
Program Simplification Strategies
Phase Split
From Standard to Nonstandard I: Modular Transfer
Superfluous Guard Elimination
Time Elapse
Precondition/Invariant Discovery Strategies
Invariant via Quantifier Elimination
From Standard to Nonstandard II: The Transfer Principle and Symbolic Computation in Mathematica
Differential Invariant
Iteration Count
Cast to Shadow
Implementation and Experiments
References
A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx
Introduction
Preliminaries
Notation
Finding Error States through Search
Guided Search
The Box-Based Distance Measure
A Trajectory-Based Distance Measure
The Box-Based Approximation
Experiments
Case Studies
Experimental Results
Conclusions
References
Hardware Verification
An Axiomatic Memory Model for POWER Multiprocessors
Introduction
Background: The POWER Memory Model
Subtleties of the POWER Memory Model
The Operational Specification
The Axiomatic Specification
Axiomatic Candidate Executions
Overview of the Specification
Examples
Formal Specification
Experimental Validation
Proof of Equivalence to the Operational Specification
Operational to Axiomatic
Axiomatic to Operational
Evaluating the Axiomatic Specification with a SAT Solver
References
nuTAB-BackSpace: Rewriting to Normalize Non-determinism in Post-silicon Debug Traces
Introduction
The BackSpace Framework
Background
Trace Buffers
Abstraction
Semi-Thue Systems
nuTAB-BackSpace
Formalizing the Intuition
Algorithm
Correctness
Experiments
Simulation-Based Evaluation
Case Study: The Leon3 SoC Hardware Prototype
Conclusion and Future Work
References
Incremental, Inductive CTL Model Checking
Introduction
Preliminaries
Algorithm
An Outline of IICTL
Forall-Exists Generalization
Refinements
Fairness
Results
Conclusion
References
Security
Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement
Introduction
Overview
Technical Description
Runtime Checks for Safety Properties
JavaScript Prototype
Experimental Evaluation
Results
Related Work
References
Automatic Quantification of Cache Side-Channels
Introduction
Preliminaries
Quantifying Information Leaks
Static Analysis of Channels
Cache Channels
Caches
Two Adversary Models Observing the Cache
Abstract Domains for Cache Analysis
Counting Cache States
Concrete States Respecting may
Concrete States Respecting must
Concrete States Respecting must and may
Counting for Probing Adversaries
Case Study
Tool Support
Target Implementations
Improving Precision by Partitioning
Results and Security Interpretation
Prior Art
Conclusions and Future Work
References
Secure Programming via Visibly Pushdown Safety Games
Introduction
Overview
An Example Policy-Weaving Problem: Filter on MiniCap
Policy-Weaving Filter via Safety Games
Policy Weaving as a Safety Game
Definition of the Policy-Weaving Problem
From Policy Weaving to Safety Games
Solving SEVPA Safety Games with Scaffolds
Definition and Key Properties of Scaffolds
An Algorithm Parametrized on Scaffolds
Experiments
Related Work
References
Verification and Synthesis
Alternate and Learn: Finding Witnesses without Looking All over
Introduction
Motivating Examples and Overview
Alternating Scope Expansion
Learning Pertinent Scopes
Preliminaries and Intra-procedural Analysis
Backward, Forward and Alternating Expansions
Alternating Expansion
Learning for Efficient Expansion
Examples Illustrating the Learning Algorithm
Evaluation
Related Work
Conclusions
References
A Complete Method for Symmetry Reduction in Safety Verification
Introduction
Related Work
Preliminaries
Symmetry
State Interpolation
Motivating Examples
Symmetry Reduction Algorithm
Experimental Evaluation
Conclusion
References
Synthesizing Number Transformations from Input-Output Examples
Introduction
Motivating Examples
Overview of the Synthesis Approach
Number Transformations
Number Transformation Language Ln
Data Structure for a Set of Expressions in Ln
Synthesis Algorithm
Combining Number Transformations with Syntactic String Transformations
The Combination Language Lc
Data Structure for Representing a Set of Expressions in Lc
Synthesis Algorithm
Experiments
Related Work
Conclusions
References
Tool Demonstration Papers
Acacia+, a Tool for LTL Synthesis
Introduction
Underlying Approach
Tool Description
Application Scenarios
References
MGSyn: Automatic Synthesis for Industrial Automation
Introduction
Modeling Industrial Automation Processes with Games
Example: Synthesizing Executable Code for FESTO MPS
Back-end Engine and Execution Platform Mapping
Concluding Remarks
References
OpenNWA: A Nested-Word Automaton Library
Introduction
NWAs
The OpenNWA library
Automata-Theoretic Operations
Client Information
Inter-operability with WPDSs
Uses of OpenNWA
Related work
References
Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification
Introduction
The Implementation and Architecture of Ufo
Preprocessing Phase
Analysis Phase
Instantiations of Ufo
Conclusion
References
SAFARI: SMT-Based Abstraction for Arrays with Interpolants
Introduction
The Tool
Discussion
Experiments
References
Bma: Visual Tool for Modeling and Analyzing Biological Networks
Introduction
Designing Biological Networks
Analyzing Biological Networks
Conclusion
References
APEX: An Analyzer for Open Probabilistic Programs
Introduction
How APEX Works
Automaton Construction
Equivalence Checking
Comparison with Other Tools
Novel Features
References
Recent Developments in FDR
Introduction
New Techniques and Features
Technical Details, Availability and Usage
References
A Model Checker for Hierarchical Probabilistic Real-Time Systems
Introduction
Modeling with PRTS
System Analysis
Simulation
Verification
Implementation and Experiments
Conclusion
References
SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs
Introduction
SymDiff
Interface for Source Languages
C Front End
Conclusion and Related Work
References
Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems
Tool Overview
System Description Language
Implementation Details and Optimizations
Multi-core Architecture
Experimental Results and Future Works
References
HybridSAL Relational Abstracter
Introduction
Relational Abstraction of Linear Systems
The HybridSal Relational Abstracter
Related Work and Conclusion
References
Euler: A System for Numerical Optimization of Programs
Introduction
Using Euler
System Internals
Results
References
SPT: Storyboard Programming Tool
Introduction
Overview: Linked List Deletion
Algorithm
Tool Architecture
Experiments and Tool Experiences
References
CSolve: Verifying C with Liquid Types
Introduction
Architecture, Use, and Availability
Example
References
passert: A Tool for Debugging Parallel Programs
Introduction
The Parallel Assertion Language
Syntax
Assertion Semantics
Applicability of Parallel Assertions to Real World Bugs
Tool Design
Response to Assertion Failure
Timing modes
Strict Timing
Relaxed Timing
Results
Conclusion
References
TRACER: A Symbolic Execution Tool for Verification
Introduction
State-Of-The-Art Interpolation-Based Verification Tools
How tracer Works
Usage and Implementation
Experience with Benchmarks
References
Joogie: Infeasible Code Detection for Java
Introduction
Joogie Overview
Bytecode Translation
Infeasible Code Detection
Experiments
Conclusion
References
HECTOR: An Equivalence Checker for a Higher-Order Fragment of ML
Introduction
Theory and Implementation
Examples and Experiments
Related Work, Conclusions and Further Directions
References
Resource Aware ML
Introduction
The Prototype Implementation
Experiments
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken