*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--16h00                     *
*                         Salle W (Toits du DI)                     *
*                    ENS  45 rue d'Ulm  75005 Paris                 *
*********************************************************************

***  Vendredi 25 fevrier 2011, 14h00-15h00 *************************

Automatic Inference of Access Permissions

Pietro Ferrara (ETH Zurich)

joint work with Peter Mueller


Re'sume'/ Abstract:

Access permissions are an expressive foundation for the verification of
imperative programs; they simplify framing and provide a basis for
reasoning about concurrent code.  They are used in a number of modern
verification approaches such as those based on separation logic or implicit
dynamic frames.  However, access permissions increase the annotation
overhead because programmers need to specify for each program component
which permissions it requires from or provides for its clients.

In this talk, we present a new static analysis based on abstract
interpretation to infer access permissions automatically.  Our analysis
computes a constraint system that captures the required access permissions
for each heap location at each program point, which is then solved using
linear programming.  We developed our analysis for the programming language
Chalice.  Experimental results demonstrate that our analysis is fast and is
able to infer almost all the access permissions for our case studies.


*********************************************************************
Pour recevoir l'annonce par courrier electronique:
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************