Verification, Model Checking, and Abstract Interpretation

Name: Verification, Model Checking, and Abstract Interpretation | 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012, Proceedings

Viktor Kuncak Andrey Rybalchenko(Herausgeber*in)

Springer (Verlag)

1. Auflage

Erschienen am 21. Januar 2012

X, 457 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-27940-9 (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
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

Systemvoraussetzungen

Als PDF speichern Als Link merken