Formal Verification of Object-Oriented Software

1. Front Matter

   PDF

2. Invited Papers

   1. Modular Verification of Object-Based Programs

      • Anindya Banerjee

      Pages 1-2

   2. The COST IC0701 Verification Competition 2011

      • Thorsten Bormer, Marc Brockschmidt, Dino Distefano, Gidon Ernst, Jean-Christophe Filliâtre, Radu Grigore et al.

      Pages 3-21

   3. The Practical Application of Formal Methods: Where Is the Benefit for Industry?

      • James J. Hunt

      Pages 22-32

   4. Isolation Types and Multi-core Architectures

      • Alan Mycroft

      Pages 33-48

   5. Modelling Adaptable Distributed Object Oriented Systems Using the HATS Approach: A Fredhopper Case Study

      • Peter Y. H. Wong, Nikolay Diakov, Ina Schaefer

      Pages 49-66

3. Contributed Papers

   1. Modeling and Analyzing the Interaction of C and C++ Strings

      • Gogul Balakrishnan, Naoto Maeda, Sriram Sankaranarayanan, Franjo Ivančić, Aarti Gupta, Rakesh Pothengil

      Pages 67-85

   2. Integration of Bounded Model Checking and Deductive Verification

      • Bernhard Beckert, Thorsten Bormer, Florian Merz, Carsten Sinz

      Pages 86-104

   3. A Probabilistic Framework for Object-Oriented Modeling and Analysis of Distributed Systems

      • Lucian Bentea, Olaf Owe

      Pages 105-122

   4. Automated Detection of Non-termination and NullPointerExceptions for Java Bytecode

      • Marc Brockschmidt, Thomas Ströder, Carsten Otto, Jürgen Giesl

      Pages 123-141

   5. Juggrnaut – An Abstract JVM

      • Jonathan Heinen, Henrik Barthels, Christina Jansen

      Pages 142-159

   6. A Verified Implementation of Priority Monitors in Java

      • Ángel Herranz, Julio Mariño

      Pages 160-177

   7. Scheduler-Specific Confidentiality for Multi-threaded Programs and Its Logic-Based Verification

      • Marieke Huisman, Tri Minh Ngo

      Pages 178-195

   8. A Formal Model of User-Defined Resources in Resource-Restricted Deployment Scenarios

      • Einar Broch Johnsen, Rudolf Schlatte, S. Lizeth Tapia Tarifa

      Pages 196-213

   9. A \(\mathbb{K}\)-Based Formal Framework for Domain-Specific Modelling Languages

      • Vlad Rusu, Dorel Lucanu

      Pages 214-231

   10. Verification of Information Flow Properties of Java Programs without Approximations

       • Christoph Scheben, Peter H. Schmitt

       Pages 232-249

4. Back Matter

   PDF

This book presents the thoroughly refereed post-conference proceedings of the International Conference on Formal Verification of Object-Oriented Software, FoVeOOS 2011, held in Turin, Italy, in October 2011 – organised by COST Action IC0701. The 10 revised full papers presented together with 5 invited talks were carefully reviewed and selected from 19 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 2011 aimed to foster collaboration and interactions among researchers in this area.

• distributed systems
• formal methods
• model checking
• modeling languages
• programs

• Institute for Theoretical Informatics, Karlsruhe Institute of Technology, Karlsruhe, Germany

  Bernhard Beckert

• Dipartimento di Informatica, Università di Torino, Italy

  Ferruccio Damiani

• Royal Institute of Technology, Stockholm, Sweden

  Dilian Gurov

Policies and ethics