********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle R, etage -1 * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* Les seminaires du mois de juillet auront lieu en salle S15 ********************************************************************* *** Vendredi 5 juillet 2002 **** 14h00 ****************************** Jens Palsberg (Purdue University) Compiling with Code-Size Constraints. Most compilers ignore the problems of limited code space in embedded systems. Designers of embedded software often have no better alternative than to manually optimize the source code or even the compiled code. Besides being tedious and error-prone, such manual optimization results in obfuscated code which is difficult to maintain and reuse. In this talk we present a code-size-directed compiler. We phrase register allocation and code generation as an integer linear programming problem where the desired bound on the code size is expressed as an additional constraint. Our experimental results show that our compiler, when applied to two commercial microcontrollers, can generate code that is as compact as carefully crafted code. Joint work with Mayur Naik. *** Vendredi 12 juillet 2002 **** 14h00 ***************************** Kwangkeun YI (KAIST, Daejon, Core'e, visiteur de l'ENS) Static Monotonicity Analysis for Lambda-definable Functions over Lattices Re'sume' : We employ static analysis to examine monotonicity of functions defined over lattices in a Lambda calculus augmented with constants, branching, meets, joins and recursive definitions. The need for such a verification procedure has arisen in our work on a static analyzer generator called Zoo, in which the specification of static analysis (input to Zoo) consists of finite-height lattice definitions and function definitions over the lattices. Once monotonicity of the functions is ascertained, the generated analyzer is guaranteed to terminate. (co-work with Andrzej Murawski, and has been presented to the 3rd Int'l Workshop on Verification, Model Checking, and Abstract Interpretation, Jan. 2002) ********************************************************************* Relache du 19 juillet au 27 septembre 2002. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr WWW: http://www.di.ens.fr/~cousot/annonceseminaire.html *********************************************************************