Formal Verification of Object-Oriented Software: International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers

by Bernhard Beckert (Editor), Claude Marché (Editor)

Overview

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.

Product Details

ISBN-13:	9783642180699
Publisher:	Springer Berlin Heidelberg
Publication date:	03/11/2011
Series:	Lecture Notes in Computer Science , #6528
Edition description:	2011
Pages:	199
Product dimensions:	6.10(w) x 9.25(h) x 0.02(d)

Table of Contents

From a Proven Correct Microkernel to Trustworthy Large Systems June Andronick 1

Static Contract Checking with Abstract Interpretation Manuel Fähndrich Francesco Logozzo 10

Abstract Compilation of Object-Oriented Languages into Coinductive CLP(X): Can Type Inference Meet Verification? Davide Ancona Andrea Corradi Giovanni Lagorio Ferruccio Damiani 31

Validating Timed Models of Deployment Components with Parametric Concurrency Einar Broch Johnsen Olaf Owe Rudolf Schlatte Silvia Lizeth Tapia Tarifa 46

Verification of Software Product Lines with Delta-Oriented Slicing Daniel Bruns Vladimir Klebanov Ina Schaefer 61

Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas Christoph D. Gladisch 76

Sawja: Static Analysis Workshop for Java Laurent Hubert Nicolas Barré Frédéric Besson Delphine Demange Thomas Jensen Vincent Monfort David Pichardie Tiphaine Turpin 92

CVPP: A Tool Set for Compositional Verification of Control-Flow Safety Properties Marieke Huisman Dilian Gurov 107

Specifying Imperative ML-Like Programs Using Dynamic Logic Séverine Maingaud Vincent Balat Richard Bubel Reiner Hähnle Alexandre Miquel 122

Dynamic Frames in Java Dynamic Logic Peter H. Schmitt Mattias Ulbrich Benjamin Weiβ 138

A Refinement Methodology for Object-Oriented Programs Asma Tafat Sylvain Boulmé Claude Marché 153

A Dynamic Logic for Unstructured Programs with Embedded Assertions Mattias Ulbrich 168

JMLUnit: The Next Generation Daniel M. Zimmerman Rinkesh Nagmoti 183

Author Index 199