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

                             Lundi 2 juin, 10h30

                               ----------------
                               Sigurd Schneider
                               ----------------

                             Saarland University

           =======================================================
                       Towards Verification of GVN-CSE
           on a Functional Intermediate Language with System Calls
           =======================================================

We present a semantic specification of a common subexpression elimination
(CSE) based on global value numbering (GVN) in the setting of a functional
intermediate language. The language includes system calls and expressions that
may err (division by zero). Semantic preservation for GVN-CSE is shown via
induction. So far, we have implemented and verified copy propagation and
constant folding against the specification; the implementation of GVN analysis
is in progress.