Verification, Model Checking, and Abstract Interpretation
13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012, Proceedings
Published on 21. January 2012
X, 457 pages
978-3-642-27940-9 (ISBN)
Description
This book constitutes the refereed proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012, held in Philadelphia, PA, USA, in January 2012, co-located with the Symposium on Principles of Programming Languages, POPL 2012. The 26 revised full papers presented were carefully reviewed and selected from 70 submissions. The papers cover a wide range of topics including program verification, model checking, abstract interpretation, static analysis, deductive methods, program certification, debugging techniques, abstract domains, type systems, and optimization.
More details
Other editions
Additional editions
Viktor Kuncak | Andrey Rybalchenko
Verification, Model Checking, and Abstract Interpretation
13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012, Proceedings
Book
01/2012
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title Page
- Preface
- Organization
- Table of Contents
- Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data
- Introduction
- Programs
- Specification Logic
- Reasoning about Programs without Procedure Calls
- Pre/Post Condition Reasoning
- Invariant Synthesis
- A Sound Decision Procedure Based on Abstraction
- Reasoning about Programs with Procedure Calls
- Pre/Post Condition Reasoning
- Synthesis of Procedure Summaries
- Experimental Results
- Conclusions and Related Work
- References
- Software Verification with Liquid Types
- Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs
- Introduction
- Course History and Format
- Format
- Prerequisites
- Aims and Principles
- No More LSD Trip Proofs!
- Teach Semantics, Not Proof Assistants
- Teach Proofs, Not Proof Scripts
- Teach Proofs, Not Logic
- Do Not Let the Proof Assistant Dominate Your Presentation
- Executability Matters
- Teaching Isabelle
- Semantics
- IMP
- Compiler
- Typed IMP
- Static Analyses
- Security Type Systems
- Hoare Logic
- Abstract Interpretation
- Conclusion
- References
- Whale: An Interpolation-Based Algorithm for Inter-procedural Verification
- Introduction
- Motivating Example
- Preliminaries
- Inter-procedural Reachability Graphs
- The Whale Algorithm
- Implementation and Evaluation
- Related Work
- Conclusion and Future Work
- References
- Synchronizability for Verification of Asynchronously Communicating Systems
- Introduction
- Motivation: Singularity Channel Contracts
- Preliminaries
- Behaviors as State Machines
- Verification Objective
- Synchronizability
- Deciding Trace Synchronizability
- Experiments with Singularity Channel Contracts
- Related Work
- Conclusion
- References
- On the Termination of Integer Loops
- Introduction
- Preliminaries
- Integer Piecewise Linear Loops
- Integer Linear Constraints Loops
- Counter Programs
- Termination of IPL Loops
- The Reduction
- Proof of Correctness
- Examples of Piecewise-Linear Operations
- Reduction to ILC Loops
- Encoding Tk with Integer Linear Constraints
- Encoding Ak with Integer Linear Constraints
- Encoding Fk with Integer Linear Constraints
- An Undecidable Extension of ILC Loops
- Simulation of Petri Nets
- Related Work
- Conclusion
- References
- Verification of Gap-Order Constraint Abstractions of Counter Systems
- Introduction
- Preliminaries
- Properties of Monotonicity Graphs
- Results on the Reachability Relation in GCS
- Checking Fairness
- Checking Fairness for Simple GCS
- Checking Fairness for Unrestricted GCS
- The Constrained Branching-Time Temporal Logic (GCCTL*)
- Concluding Remarks
- References
- On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking
- Multi-Rooted Binary Decision Diagrams Package
- Encoding
- Rounding
- Non-negative Integer Exponent
- Multiplicative Inverse of Positive Integer
- Composition
- Model Checking with MRBDD
- Modeling Approach
- Model Checking Algorithms
- Experimental Results
- Synchronous Leader Election
- Birth-Death Process
- Conclusions and Further Work
- References
- Regression Verification for Multi-threaded Programs
- Introduction
- Equivalence of Multi-threaded Programs
- Assumptions, Preprocessing and Mapping
- Global Preprocessing
- Mapping
- First Proof Rule
- Function Transformation: From f to f"0362f.
- The Proof Rule
- Definitions
- Soundness
- The Value of Partial Success
- Second Proof Rule
- Recursion-Bounded Abstraction
- The Proof Rule
- Soundness of the Proof Rule
- Conclusion and Future Work
- References
- Crowfoot: A Verifier for Higher-Order Store Programs
- Introduction
- Programming and Assertion Languages
- Programming Language Featuring Higher-Order Store
- Assertion Language
- Crowfoot Input Language
- Deep Framing
- Specification of the Running Example
- Automation of Program Verification
- Overview
- Symbolic Execution Engine
- Entailment Provers
- Theoretical Basis
- Excerpt from the Verification of the Running Example
- Related and Future Work
- References
- Synthesizing Protocols for Digital Contract Signing
- Introduction
- Fair Non-repudiation Protocols
- LTL Objectives for the Protocols
- Co-synthesis
- Protocol Co-synthesis
- Failure of Classical and Weak Co-synthesis, and the Need for a TTP
- Assume-Guarantee Solutions Are Attack-Free
- Analysis of Existing Protocols
- Conclusion
- References
- Model Checking Information Flow in Reactive Systems
- Introduction
- Preliminaries
- The Temporal Logic SecLTL
- Examples
- Model Checking SecLTL
- Complexity of the Model Checking Problem for SecLTL
- Restricted SecLTL
- Extension to Branching Time
- Related Work
- Conclusion
- References
- Splitting via Interpolants
- Introduction
- Example
- Preliminaries
- Splitting via Path Insensitive Interpolants
- Underlying Splitting Algorithm
- Path Insensitive Interpolation
- Experimental Evaluation
- Related Work
- Conclusion
- References
- Automatic Inference of Access Permissions
- Introduction
- Language
- Heap Analysis
- Symbolic Permissions
- Symbolic Values
- Abstract Domain
- Abstract Semantics
- Unsound Approximations
- Annotation Inference
- Permission Systems
- Inferring Constraints
- Resolution of the Constraints
- Experimental Results
- Related Work
- Conclusion
- References
- Lazy Synthesis
- Introduction
- The AMBA Case Study
- The Synthesis Problem
- The Partial Design of the AMBA Protocol
- Lazy Synthesis
- The Solve-Check-Refine Loop
- Solve
- Check
- Refine
- Symbolic Implementation
- Experiments
- Conclusions
- References
- Donut Domains: Efficient Non-convex Domains for Abstract Interpretation
- Introduction
- Donut Abstract Domains
- Lattice Structure
- Decidability of the Order
- Meet and Join Operations
- Loop Widening
- Interpretation of Tests
- Abstract Assignment
- Template-Based under-Approximations of Polyhedra
- Implementation
- Conclusions and Future Work
- References
- Inferring Canonical Register Automata
- Introduction
- Register Automata and Data Languages
- Active Learning of Canonical RAs
- Residual Data Languages
- Hypothesis Construction
- Hypothesis Validation
- Correctness and Complexity
- Example Application
- Conclusions
- References
- Alternating Control Flow Reconstruction
- Introduction
- Overview
- Parameterized Semantics for Low-Level Control Flow
- Intermediate Language
- Parameter Semantics Template
- Control Flow Semantics
- Instantiating the Parameterized Semantics
- Concrete Semantics
- Over-Approximate Semantics
- Under-Approximate Semantics
- Alternation in Control Flow Reconstruction
- Combined Semantics
- Alternation Framework
- Algorithm
- Characterizing the Reconstructed CFG
- Evaluation
- Implementation and Setup
- Experimental Results
- Current Limitations and Future Work
- Related Work
- Conclusion
- References
- Effective Synthesis of Asynchronous Systemsfrom GR(1) Specifications
- Introduction
- Preliminaries
- Expanding the Rosner Reduction to Multiple Variables
- A More General Asynchronous Interaction Model
- Proving Realizability of a Specification, and Synthesis
- Applying the Realizability Test
- Conclusions and Future Work
- References
- Sound Non-statistical Clusteringof Static Analysis Alarms
- Introduction
- Problem
- Our Solution
- Alarm Clustering Framework
- Definitions
- Alarm Clustering
- Alarm Clustering Algorithm
- Experiments
- Implementation
- Experiment Results
- Related Work
- Conclusion
- References
- Automating Induction with an SMT Solver
- Introduction
- Background on Dafny
- Verifier Architecture
- Inductive Lemmas in a Program Verifier
- The Induction Tactic
- Induction Principle
- Induction Translation
- Induction Heuristic
- Well-Founded Orders in Dafny
- Datatypes and Case Distinctions
- Multiple Bound Variables
- Overriding the Induction Heuristic
- Examples
- A Simple Program
- A Difficult Program
- Integers
- Inductive Datatypes
- Operation of the SMT Solver
- Evaluation on a Test Suite for Induction
- Induction for Ghost Methods
- Conclusion
- References
- Modeling Asynchronous Message Passing for C Programs
- Introduction
- Modeling with 4M
- Formal Model of the API
- Semantic Implementation of 4M
- 4M Implementation
- Reference Solution for Test, Debug, and Behavior Exploration
- MCAPI Model Results
- Related Work
- Conclusion and Future Work
- References
- Local Symmetry and Compositional Verification
- Introduction
- Networks and Their Symmetry Groupoids
- Local Symmetry Groupoids
- Local Reasoning on a Process Network
- Assignment of Variables and Processes
- Local Proof Rules
- Symmetry and Quotients
- Automorphisms and Balance
- Balance and Symmetry
- Symmetry-Reduced Local Invariant Computation
- Equivalent Networks and the Quotient Construction
- Pairwise Symmetry and Balance Relations
- Consequences
- Related Work, Conclusions and Open Questions
- References
- versat: A Verified Modern SAT Solver
- Introduction
- Verified Programming in Guru
- Specification
- Representation of CNF Formula
- Deduction Rules
- The answer Type
- Parser and Entry Point
- Implementation and Proof
- Array-Based Clauses and Invariants
- Conflict Analysis with Optimized Resolution
- Summary of Implementation
- Evaluation
- Related Work
- Discussion
- Conclusion and Future Work
- References
- Decision Procedures for Region Logic
- Introduction
- Preliminaries
- RL-Tableau Calculus
- Implementation of Semi-decision Procedure
- Restricted-RLE-Tableau Calculus
- Related Work
- Discussion
- References
- A General Framework for Probabilistic Characterizing Formulae
- Introduction
- Preliminaries
- General Framework
- Probabilistic Automata, Simulations, and Bisimulations
- Lifting of Relations
- Probabilistic Automata
- Simulations and Bisimulations
- Hennessy-Milner Logic for Probabilistic Automata
- Characteristic Formulae
- Simulations
- Probabilistic Simulations and Probabilistic Bisimulation
- Weak Simulations
- Probabilistic Forward Simulation for Probabilistic Automata
- Extensions
- Conclusion
- References
- Loop Invariant Symbolic Execution for Parallel Programs
- Introduction
- Loop Invariant Symbolic Execution for Sequential Programs
- Extending LISE to Parallel Programs: Challenges
- Multiprocess Loop Invariant Symbolic Execution
- Notation and Formal Framework
- Collective Assertions and Loop Invariants
- Multiprocess LISE State
- The Multiprocess LISE Next-State Function
- Example
- Soundness
- Implementation and Experiments
- Conclusion
- References
- Synthesizing Efficient Controllers
- Introduction
- Preliminaries
- Specifying Efficient Controllers
- Solving MDPs with Ratio-Objectives
- General Shape
- Policy Iteration
- Fractional Linear Program
- Linear Program
- Related Work
- Synthesis and Experimental Results
- Conclusion
- References
- Ideal Abstractions for Well-Structured Transition Systems
- Introduction
- Motivating Example
- Preliminaries
- Ideal Abstraction
- Concrete and Abstract Domain
- Widening
- Set-Widening Operators for Ideal Completions
- Petri Nets
- Lossy Channel Systems
- Depth-Bounded Processes
- Implementation and Evaluation
- Conclusion
- References
- Author Index
