********************************************************************* * 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 * ********************************************************************* *** Vendredi 2 novembre 2002 **** 14h00 ***************************** Rela^che (week-end de la Toussaint) *** Vendredi 9 novembre 2002 **** 14h00 ***************************** Rela^che *** Vendredi 16 novembre 2001 **** 14h00 **************************** Rela^che *** Mercredi 21 novembre 2001 **** 15h00 ******************************* David Monniaux (ENS) Analyse de programmes probabilistes par interpre'tation abstraite Salle des the`ses D520, Universite' Paris IX Dauphine Place du Mare'chal de Lattre de Tassigny 75775 Paris cedex 16 Me'tro : Porte Dauphine - RER C : Avenue Foch *** Vendredi 23 novembre 2001 **** 14h00 **************************** Neil JONES (DIKU, University of Copenhagen & Ecole Polytechnique & ENS) Size-change Principle for Program Termination Re'sume': The principle, assuming well-founded data, is simple: If every infinite control sequence that follows the program's control flow would cause an infinite descent in at least one value, then the program terminates for all runs and all inputs. Although quite simple, this principle seems powerful enough for many programs, and suitable for automation. A virtue is that termination is proven by analysis; the user does NOT have to provide "progress functions" or devise perhaps subtle well-founded orders (lexicographic or otherwise) to show termination. Further, it is flexible enough to handle problems such as indirect recursion and permuted variables that seem difficult for other methods automatically and without special treatment. Analysis proceeds in two phases (henceforth for a first-order functional language): First, for every call c:f->g from function f to function g in the program, a Size-Change Graph G_c is constructed. G_c registers definite equalities and definite size decreases in values. (G_c is built using known properties of base functions, and perhaps a "size analysis"to gain more precise descriptions.) A sequence of such graphs following control flow describes data flow along one computational stream. Second, the principle is tested: if every infinite call sequence leads to infinite decrease in some data, the program terminates. Surprisingly, this can be tested EXACTLY using Buechi automata. More, the complexity of the method can be determined: PSPACE is both upper and lower worst-case (as a function of the analyzed program's size). A practically more efficient graph-based algorithm has been devised (using Ramsey's theorem), tried on a number of examples, and ven been incorporated into the AGDA theorem prover at Chalmers. The approach also provides a new angle of attack on estimating programs' worst-case running times. This is current work, and will be described today or later if there is interest. *** Vendredi 23 novembre 2001 **** 15h00 **************************** Damien MASSE' (LIX, Ecole Polytechnique) Extension of transition systems, abstract interpretation. ********************************************************************* *** REPORTE' EN DE'CEMBRE ******************************************* ********************************************************************* *** Vendredi 30 novembre 2001 **** 14h00 **************************** rela^che (ICLP'01) ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************