Formal Verification of Object-Oriented Software

Name: Formal Verification of Object-Oriented Software | International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers

Bernhard Beckert Claude Marché(Herausgeber*in)

Springer (Verlag)

Erschienen am 18. Januar 2011

X, 199 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-18070-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
Preface
Organization
Table of Contents
From a Proven Correct Microkernel to Trustworthy Large Systems
Introduction
A Proven Correct OS Kernel
Trustworthy, Large Systems
References
Static Contract Checking with Abstract Interpretation
Introduction
CodeContracts by Example
Specification
Static Checking
The Analysis
Basic Framework
Fact Inference
NonNull Analysis
Numerical Analysis
Floating Point Values
Arrays and Collections
Checking
Contract Inference
Practical Considerations
Conclusions
References
Abstract Compilation of Object-Oriented Languages into Coinductive CLP(X): Can Type Inference Meet Verification?
Introduction
Background: Coinductive LP/SLD and CLP(X)
Abstract Compilation by Example
Formalization
A Prototype Implementation of Coinductive CLP(X)
Conclusion
References
Validating Timed Models of Deployment Components with Parametric Concurrency
Introduction
Concurrent Objects in Creol
Deployment Components with Parametric Concurrency
Example: A Distributed Shopping Service
Operational Semantics
Simulating and Testing the Example
Related Work
Conclusions and Future Work
References
Verification of Software Product Lines with Delta-Oriented Slicing
Introduction
Delta-Oriented Programming of Software Product Lines
Delta-Oriented Formal Specification of Software Product Lines
Delta-Oriented Slicing
Proof Reuse for Changed Methods
Related Work
Conclusions
References
Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas
Introduction
Background and Related Work
The Basic Idea of Our Approach
KeY's Dynamic Logic with Updates
Model Generation by Iterative Update Construction
Heuristics for Update Construction from Formulas
Update Construction from Ground Formulas
Update Construction from Quantified Formulas
Experiments, Conclusions, and Future Work
References
Sawja: Static Analysis Workshop for Java
Existing Libraries for Manipulating Java Bytecode
High-Level Representation of Classes
Intermediate Representation
Overview of the IR Language
IR Generation
Experiments
Complete Programs
API of Complete Programs
Construction of Complete Programs
References
CVPP: A Tool Set for Compositional Verification of Control-Flow Safety Properties
Introduction
Program Model and Logic
Model and Logic
Control-Flow Structure and Behaviour
Framework for Compositional Verification
Tool Support for Compositional Verification
Typical Verification Scenarios
Open System Verification
Modular Verification
Non-compositional Verification
Wrapper Tools for Standard Verification Scenarios
Executing the Verification Scenarios
Generating Maximal Flow Graphs for a Behavioural Property
Closed System Model Checking of a Behavioural Property
Conclusion
References
Specifying Imperative ML-Like Programs Using Dynamic Logic
Introduction
Dynamic Logic
Programming Language
Syntax
Operational Semantics
Well-Formedness of Stores
Logical System
Symbolic Expressions
Updates
Formulas
Symbolic Evaluation
Deduction Rules
Semantics
Invariance Properties
Interpreting Symbolic Values and Updates
Interpreting Formulas and Sequents
Specification and Verification of a Recursive Function
Conclusion
References
Dynamic Frames in Java Dynamic Logic
Introduction
Motivating Example
Java Dynamic Logic with an Explicit Heap Model
Syntax and Semantics
Sequent Calculus
Heap Model
Symbolic Execution
Contracts and Proof Obligations
Method Contracts
Dependency Contracts
Conclusions
References
A Refinement Methodology for Object-Oriented Programs
Introduction
Preliminaries
Deductive Verification of Contracts
Refinement
Model Fields
Ownership
Ownership and Model Fields
Language Setting
Pack/Unpack forModel Fields
Invariant Preservation
A Refinement Methodology
Hiding Effects Using Datagroups in Assigns Clauses
Modular Reasoning on Shared State: The Observer Pattern Example
Conclusions, RelatedWork and Perspectives
References
A Dynamic Logic for Unstructured Programs with Embedded Assertions
Introduction
Syntax and Semantics
Syntax
Semantics
Symbolic Execution
Invariant Rules
Program Modifications
Simple Invariant Rule
Invariant Rule with Termination
Improved Invariant Rule
Related Work
Conclusion
References
JMLUnit: The Next Generation
Introduction
Background
Unit Testing
The Java Modeling Language
JMLUnit
Shortcomings of JMLUnit
JMLUnitNG: Improvements to JMLUnit
Test Data Generation
Context-Dependent Test Data
Iterators and Lazy Test Generation
Comparison of JMLUnit and JMLUnitNG
Related Work
Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken