To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 09/02/10 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                           Mardi 9 février, 14h30

                            -------------------
                            Tahina Ramananandro
                            -------------------

                                   INRIA

         =========================================================
         A machine-checked formalization of concrete object layout
                        for C++ multiple inheritance
         =========================================================

Formal methods are frequently used to reason about object-oriented programming 
languages at the source-code level, but low-level implementations are 
currently lacking the support for machine-checked verification. Our work aims 
at filling in the gap between an abstract formalization of C++ multiple 
inheritance and a concrete implementation of object layout.

This talk will present a formalization of C++ multiple inheritance and object 
layout with the Coq proof assistant. In a previous work, Wasserrab, Nipkow et 
al. [1] abstractly formalized multiple inheritance following the Rossie-
Friedman subobject model [2]. We extend this work by choosing a realistic 
concrete object layout and formalizing it within the framework of the CompCert 
memory model by Leroy and Blazy [3]. We then show that our concrete object 
layout matches the abstract formalization.

This work is a first step towards a verified compiler for a subset of C++. It 
may also help reasoning about application binary interfaces (ABI) for C++ [4] 
to prove their consistency or to find bugs.

References :
[1] Daniel Wasserrab, Tobias Nipkow, Gregor Snelting and Frank Tip. An 
operational semantics and type safety proof for multiple inheritance in C++. 
Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented 
programming systems, languages, and applications (OOPSLA), p. 345-362, 2006, 
Portland, Oregon, United States
[2] Jonathan G. Rossie, Jr. , Daniel P. Friedman, An algebraic semantics of 
subobjects, Proceedings of the tenth annual conference on Object-oriented 
programming systems, languages, and applications (OOPSLA), p.187-199, October 
15-19, 1995, Austin, Texas, United States 
[3] Xavier Leroy and Sandrine Blazy. Formal verification of a C-like memory 
model and its uses for verifying program transformations. Journal of Automated 
Reasoning, 41(1):1-31, 2008.
[4] C++ ABI summary. http://www.codesourcery.com/public/cxx-abi