Formal Verification of Object-Oriented Software
International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers
Published on 18. January 2011
X, 199 pages
978-3-642-18070-5 (ISBN)
Description
This book presents the thoroughly refereed post-conference proceedings of the International Conference on Formal Verification of Object-Oriented Software, FoVeOOS 2010, held in Paris, France, in June 2010 - organised by COST Action IC0701.
The 11 revised full papers presented together with 2 invited talks were carefully reviewed and selected from 21 submissions. Formal software verification has outgrown the area of academic case studies, and industry is showing serious interest. The logical next goal is the verification of industrial software products. Most programming languages used in industrial practice are object-oriented, e.g. Java, C++, or C#. FoVeOOS 2010 aimed to foster collaboration and interactions among researchers in this area.
More details
Other editions
Additional editions
Bernhard Beckert | Claude Marché
Formal Verification of Object-Oriented Software
International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers
Book
01/2011
Springer
€53.49
Shipment within 5-7 days
Content
- 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
