To: seminaire@pauillac.inria.fr
From: Bruno.Barras@inria.fr
Subject: SEM - INRIA : LogiCal - 20/04/01 - Paris - FR

      Vous pouvez maintenant vous abonner à nos annonces de séminaires
             http://pauillac.inria.fr/seminaires/subscribe.html


                             S E M I N A I R E
                                         . ___ 
                           /   _   _      /   _   /
                          /   / \ / \  / /   __| /
                         |___ |_/ |_/ / |__ |_/ |_
       ___      .                  /    
      /    ___   __  /_  _   /   _/        /| /|  _   __ __ _       _ 
     /    /   / /_  /   __| /             / |/ | / \ /_ /  / \ | / __|
    |___ /   / __/ |_  |_/ |_            /     | |_/__/ |_ |_/ |/ |_/
                                                
                          I N R I A - Rocquencourt
                       Salle de conference du Bat 11

                          Vendredi 20 avril, 10h30

                              ---------------
                              Marieke Huisman
                              ---------------

                    INRIA Sophia-Antipolis, Projet Lemme

              ===============================================
              The LOOP project: Reasoning about Java programs
              ===============================================


    The LOOP project (for Logic of Object-Oriented Programming) is a joint
    project  between the  University  of Nijmegen  and  the University  of
    Dresden.   Initially,  this   project  focused   on   reasoning  about
    object-oriented  specification languages,  but later  a branch  of the
    project  also aimed  at verification  of object-oriented  programs (in
    particular Java program).

    The work within this Java branch concentrates on three things:

    - describing a  semantics for  Java (in type  theory and  higher order
      logic)

    - building  a compiler  to translate  a Java  program into  a semantic
      description that  can be used as input for a  theorem prover (PVS or
      Isabelle)

    - actually reasoning about Java programs

    Currently, the main focus of  application is JavaCard, a stripped down
    version of  Java for programming  the next generation of  smart cards.
    This work is part of the European Project Verificard.

    In my talk I will give  a general overview of the LOOP project, discus
    the underlying semantics  and the development of the  LOOP compiler. I
    will talk about  new developments on extending the  LOOP compiler with
    JML. The last part of the talk  I will concentrate on my own work, and
    discuss  some example  verifications and  the  verification techniques
    that we used (in particular, a Hoare logic tailored towards Java).