********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle W, 4e`me e'tage, toits du DMI * * DMI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 7 novembre 1997 **** 14h00 ***************************** Advanced Compilation Techniques for Logic Programs based on Abstract Interpretation and Program Transformation German PUEBLA (Universidad Politecnica de Madrid & LIENS) Re'sume' : We briefly present some contributions to the implementation and application of abstract interpretation techniques for both program optimization and validation. The techniques to be presented have been implemented on the CIAO system at the CLIP group of the Technical University of Madrid. We will present several novel analysis algorithms which allow efficiently reusing previous analysis information in an incremental way while being competitive or even better than non-incremental algorithms for the non-incremental case. We will then consider the analysis of unrestricted, real-life logic programming languages. We will also present an algorithm for multiple specialization of programs based on abstract interpretation which allows generating several versions of predicates for different uses and its application to automatic parallelization. Then we will introduce some optimization techniques for logic programs with dynamic scheduling. Last, we will discuss some aspects of the use of abstract interpretation for validation and debugging of constraint logic programs. *** Vendredi 14 novembre 1997 **** 14h00 **************************** Relache, Workshop on Abstract Interpretation, KAIST, Taejon (Taeduk Science Complex), Korea, 10--14 november 1997. *** Vendredi 21 novembre 1997 **** 14h00 **************************** Building abstract domains as solutions of equation systems: A logical view Francesca SCOZZARI (DIPISA & LIX) Re'sume' : In the context of static program analysis by abstract interpretation, we are particularly interested in developing systematic methods to specify domains as solutions of suitable domain equations. The starting point is a refinement operator, the Heyting completion, which interprets the Cousot&Cousot reduced cardinal power. An intuitionistic propositional theory is used to represent abstract objects in the refined domains. An example of application in logic programming is presented, to perform groundness analyses. Other function-based refinement operators are studied, as solution of domain equation systems. A propositional linear theory is used to represent abstract objects. This refinement operators provide a link between the notion of completeness and the solution of a domain equation system. *** Vendredi 28 novembre 1997 **** 14h00 **************************** Escape Analysis : Correctness, Implementation, and Experimental Results Bruno BLANCHET (ENS & INRIA) Re'sume' : We describe an analysis aimed at determining whether the lifetime of data exceeds its static scope, and named escape analysis. In this talk, we quickly define the notion of correctness of the analysis which we have used to in our proofs. Contrary to previous work, our definition of correctness takes into account all the features of functional languages, even imperative features and polymorphism. We describe our implementation, which has been designed to fit in the small complexity bound of O(n (log n)^2) where n is the size of the analyzed program. We have included it in the Caml Special Light compiler (an implementation of ML), and applied it to very large programs. Escape analysis has been applied to stack allocation. We improve the optimization technique, by determining minimal lifetime for stack allocated data, and using inlining. We manage to stack allocate 25% of data in the theorem prover Coq. We analyzed the effect of this optimization, and noticed that its main effect is to improve data locality, which is important for efficiency. ******************************************************************** recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr WWW: http://www.ens.fr/~cousot/annonceseminaire.html *********************************************************************