*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h30                     *
*                           Salle S16, etage -1                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************


*** Vendredi 25 novembre 2005 ***************************************

Olin Shivers (Georgia Tech)

Environment analysis with $\Delta$CFA 

Abstract: 

The lambda expression provides, as a single linguistic construct, all three     
fundamental program structures: data structure, environment structure, and      
control structure. This universality is one of the sources of its power and     
centrality in programming languages, but it is also the reason why lambda is    
so difficult to analyse. Because these three kinds of structure come together   
in lambda, a program analysis that handles lambda must simultaneously handle    
all three facets of the construct. Thus a control-flow analysis for             
lambda-based programs must be, at the same time, an environment- and data-flow  
analysis, and vice versa.                                                       
                                                                                
While techniques to analyse lambda-based programming languages have been        
around for quite some time, the weakest facet of these analyses has been        
the handling of environment structure. For example, the nature of the           
environment abstractions used in the $k$-CFA hierarchy acts as a fundamental    
barrier to certain classes of analysis.                                         
                                                                                
I will present a new analysis, $\Delta$CFA, which exploits an                   
environment/control abstraction based on a variant of \emph{procedure           
strings}, a record of procedure entries and exits. The new analysis permits     
more precise reasoning about environment structure, enabling new classes of     
optimisation.                                                                   
                                                                                
This work is a joint effort with my student, Matthew Might.                     
                                                                                
---------------------------------------------------------------------------- 
Olin Shivers received his undergraduate degree in Computer Science and          
Mathematics from Yale University; his undergraduate advisor was Alan Perlis.    
His doctoral work in program analysis was done at Carnegie Mellon, under the    
supervision of Peter Lee and Allen Newell. Since then, he has held positions    
at Bell Labs, and the University of Hong Kong and the MIT AI Lab, before        
joining the faculty at Georgia Tech, where he currently teaches and does        
research in programming languages. Prof. Shivers has also started several       
companies; his most recent is Smartleaf, which provides scalable                
portfolio-analysis technology to the financial industry.                        
*********************************************************************
Pour recevoir l'annonce par courrier electronique: 
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************