Verification, Model Checking, and Abstract Interpretation
12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011 Proceedings
Published on 19. January 2011
XI, 419 pages
978-3-642-18275-4 (ISBN)
Description
This book constitutes the refereed proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011, held in Austin, TX, USA, in January 2011, co-located with the Symposium on Principles of Programming Languages, POPL 2011. The 24 revised full papers presented together with 4 invited talks were carefully reviewed and selected from 71 initial submissions. The papers showcases state-of-the-art research in areas such as verification, model checking, abstract interpretation and address any programming paradigm, including concurrent, constraint, functional, imperative, logic and object-oriented programming. Further topics covered are static analysis, deductive methods, program certification, debugging techniques, abstract domains, type systems, and optimization.
More details
Other editions
Additional editions
Ranjit Jhala | David Schmidt
Verification, Model Checking, and Abstract Interpretation
12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011 Proceedings
Book
01/2011
Springer
€53.49
Shipment within 5-7 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Are Cells Asynchronous Circuits? (Invited Talk)
- Formal Analysis of Message Passing (Invited Talk)
- Introduction
- An Overview of MPI and Its Correctness Issues
- Symbolic Execution and Reachability Analysis for MPI
- Dynamic Analysis of MPI
- Concluding Remarks
- References
- Practical Verification for the Working Programmer with CodeContracts and Abstract Interpretation (Invited Talk)
- References
- Quality Engineering: Leveraging Heterogeneous Information (Invited Talk)
- Introduction
- Structured Operational Semantics
- Standard SOS
- Control Flow Analysis: The One Point Domain
- SOS-Based Odd/Even Analysis
- Property Oriented Expansion
- Eliminating All Partial Redundancies
- Case Study: Virtual Call Resolution
- Unifying Models
- Conclusions and Perspectives
- References
- More Precise Yet Widely Applicable Cost Analysis
- Introduction
- Preliminaries
- Cost Relations: The Common Target of Cost Analyzers
- Single-Argument Recurrence Relations
- An Informal Account of Our Approach
- Inference of Precise Upper Bounds
- Constant Cost Relations
- Non-constant Cost Relations
- Non-deterministic Non-constant Cost Relations
- The Dual Problem: Lower Bounds
- Experiments and Conclusions
- Conclusions
- References
- Refinement-Based CFG Reconstruction from Unstructured Programs
- Introduction
- Preliminaries
- The Propagate and Refine Procedure
- Value Analysis with Precision Requirements (VAPR)
- Basic Intuitions on the Propagate and Refine Procedure
- The PaR Procedure for VAPR
- Relative Completeness
- Experiments
- Related Work
- Conclusion
- References
- SAT-Based Model Checking without Unrolling
- Introduction
- Definitions
- Applying Induction Incrementally
- Informal Description
- Related Work
- Formal Presentation and Analysis
- Single-Core Implementation
- Parallel Implementation
- Conclusion
- References
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
- Introduction
- Background
- Presburger Arithmetic with Predicates and Functions
- An Interpolating Sequent Calculus
- Interpolation for Uninterpreted Predicates
- Presburger Arithmetic and Uninterpreted Predicates
- Quantifiers in QPA+UP Interpolants
- Interpolation for Uninterpreted Functions
- A Relational Encoding of Uninterpreted Functions
- Interpolation for PAID+UF
- Interpolation for the Theory of Extensional Arrays
- Related Work and Conclusion
- References
- Probabilistic B\"{u}chi Automata with Non-extremal Acceptance Thresholds
- Introduction
- Preliminaries
- Examples
- Decision Problems
- Expressiveness
- Simple PBAs
- Conclusions and Further Work
- References
- Synthesis of Fault-Tolerant Embedded Systems Using Games: From Theory to Practice
- Introduction
- Motivating Scenario
- Adding FT Mechanisms to Resist Message Loss
- Solving Fault-Tolerant Synthesis by Instrumenting Primitives
- System Modeling
- Platform Independent System Execution Model
- Interleaving Model (IM)
- Games
- Step A: Front-End Translation from Models to Games
- Step A.1: From PISEM to IM
- Step A.2: From IM to Distributed Game
- Step B: Solving Distributed Games
- Conversion from Strategies to Concrete Implementations
- Implementation and Case Studies
- Related Work
- Concluding Remarks
- References
- Proving Stabilization of Biological Systems
- Introduction
- Example: Skin Cells
- Stabilization Algorithm
- Experimental Results
- Conclusions
- References
- Precondition Inference from Intermittent Assertions and Application to Contracts on Collections
- Introduction
- Program Semantics
- Specification Semantics
- The Contract Precondition Inference Problem
- Basic Elements of Abstract Interpretation
- Fixpoint Strongest Contract Precondition
- Contract Precondition Inference by Symbolic Flow Analysis
- Contract Precondition Inference for Scalar Variables by Forward Symbolic Analysis
- Contract Precondition Inference by Backward Symbolic Analysis
- Contract Precondition Inference for Collections by Forward Static Analysis
- Related Work, Future Work, and Conclusions
- References
- Strengthening Induction-Based Race Checking with Lightweight Static Analysis
- Introduction
- Guiding k-Induction with Invariants: An Overview
- DMA Race Analysis
- k-Induction for Loops: Promise, and Problems
- Strengthening k-Induction for DMA Race Analysis
- Abstract Interpretation-Based Static Analysis
- Chunking
- Code Motion to Ease Analysis of Inner Loops
- Experimental Evaluation
- Related Work
- Summary
- References
- Access Nets: Modeling Access to Physical Spaces
- Introduction
- Overview
- Access Nets
- Verification of Access Properties
- Case Study: Office Security
- Related Work
- Conclusion
- References
- Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation
- Introduction
- Dynamic Pushdown Networks
- Forward Reachability
- Action Trees
- Join-Lock-Sensitive Schedules of Action Trees
- Conclusion
- References
- Verifying Deadlock-Freedom of Communication Fabrics
- Introduction
- Related Work
- xmas Primitives
- Channel Properties
- Persistency
- Life and Death of Channels
- Fairness of Sinks and Sources
- Characterizing Structural Deadlocks
- Variables
- Deadlock Equations
- Sources and Sinks
- Checking Structural Deadlocks
- Adding Reachability Constraints
- Results
- Conclusion
- References
- Static Analysis of Finite Precision Computations
- Introduction
- Modelling Finite Precision Computations
- Finite Precision Computations
- Concrete Model
- A Non Relational Abstraction
- Interval Abstraction of Values and Error Decomposition
- Transfer Functions for Arithmetic Operations
- Order-Theoretic Operations
- Fixpoint Iteration
- A Zonotopic Abstraction
- Zonotopic Abstract Domain for Real Values
- Abstract Domain for Finite Precision Computations
- Implementation and Results
- Conclusion and Future Work
- References
- An Evaluation of Automata Algorithms for String Analysis
- Introduction
- Preliminaries
- Automata Data Structures and Algorithms
- Representing Character Sets
- Primitive Automata Algorithms
- Experiments
- Related Work
- Conclusions
- References
- Automata Learning with Automated Alphabet Abstraction Refinement
- Introduction
- Alphabet Abstraction Refinement
- A Sketch of Classical Automata Learning
- Determinism Preserving Abstraction
- Automated Alphabet Abstraction Refinement
- An Example Run of the Algorithm
- Conclusion
- References
- Towards Complete Reasoning about Axiomatic Specifications
- Introduction
- Example
- Background
- Reasoning about ADTs with Abstractions
- Complete Reasoning about Single-Invocation Axioms
- Complete Reasoning about Many-Invocation Axioms
- Complete Reasoning about Conjunctive Combinations
- Complete Reasoning about Piecewise Combinations
- Related Work
- References
- String Analysis as an Abstract Interpretation
- Introduction
- Preliminary
- Motivating Example
- PDA Configuration Changes Caused by One String
- The Need
- Configuration Change
- Algorithm for Computing Minimal Configuration Changes
- The Finiteness Condition: Boundedness
- Formalizing String Analysis
- The Predicate Domain
- The Domain (CA, )
- The Galois Connection
- Abstract String Concatenation Operation
- The Widening Operator
- Example Revisited
- Related Work
- Discussion and Ongoing Work
- References
- ExplainHoudini: Making Houdini Inference Transparent
- Introduction
- Background
- Source and Assertion Languages
- Modular Contract Checking and Contract Inference
- Houdini Algorithm
- Example
- ExplainHoudini
- Cause
- Example Revisited
- Algorithm
- Optimizations
- Evaluation
- Conclusion
- References
- Abstract Probabilistic Automata
- Introduction
- Specifications and Implementations
- Abstraction and Refinement
- Refinement
- Abstraction
- Compositional Reasoning
- Conjunction
- Parallel Composition
- Completeness and Relation with CMCs
- Conclusion
- References
- Distributed and Predictable Software Model Checking
- Introduction
- Example
- Preliminaries
- Predictable Distributed Verification Algorithm
- Experiments
- References
- Access Analysis-Based Tight Localization of Abstract Memories
- Introduction
- Setting: Baseline Analyzer
- Memory Localization by Access Analysis
- Conventional Reachability-Based Localization for Procedures
- Access-Based Localization for Procedures
- Access-Based Localization for Arbitrary Code Blocks
- Experiments
- Related Work and Discussion
- References
- Decision Procedures for Automating Termination Proofs
- Introduction
- Examples
- Decision Procedure Through an Example
- Preliminaries
- POSSUM: Multiset Constraints over Preordered Sets
- Finite Multisets over Preordered Sets
- Syntax and Semantics of POSSUM Formulas
- Decision Procedure
- Further Related Work
- Conclusion
- References
- Collective Assertions
- Introduction
- Model
- Collective Assertions
- The Extended Transition System
- Implementation and Experiments
- Overview of TASS
- Collective Assertion Specification and Verification in TASS
- Scaling Experiment
- Further Examples
- Related Work
- Conclusion
- References
- Sets with Cardinality Constraints in Satisfiability Modulo Theories
- Introduction
- Example
- Decomposition in Solving BAPA Constraints
- A Simple Decision Procedure for QFBAPA
- Decomposing Conjunctions of QFBAPA Formulas
- Hypertree Decompositions
- Integration with Z3
- Evaluation
- Related Work
- References
- Author Index
