********************************************************************* * 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 6 juillet 2001 **** 14h00 ****************************** Relache (salles ENS reservees au concours) *** Vendredi 13 juillet 2001 **** 14h00 ***************************** System Zoo: towards a realistic program analyzer generator Kwangkeun YI (Research On Program Analysis System (ROPAS) KAIST (Korea Advanced Institute of Science and Technology) ropas.kaist.ac.kr, Re'publique de Core'e) !!! salle inhabituelle: Salle W, toits du DMA, 4eme e'tage. Re'sume': I am currently building a program-analysis generator (named ``Zoo'') that supports an ensemble of four frameworks of static analysis: abstract interpretation, data-flow analysis, constraint-based analysis, and model checking. The first three frameworks are presentation variations among which the user chooses one to conveniently specify how to set-up static equations from the input programs. Zoo system transforms this specification into a combination of a data-flow equation extractor and a specialized fixpoint iterator (equation solver). The last framework, model checking is used to specify queries on the equation solutions. The user specifies static properties as CTL (computational tree logic) formula. Zoo system generates a model checking procedure that checks this formula against the equation solutions. I will present the overall architecture of the system (i.e. how I view the static analysis generation), its high-level specification language, its incremental fixpoint computation method, and its anticipated uses in our version of proof-carrying-codes, which we are developing on top of our ML compiler system called nML. ********************************************************************* Relache du 20 juillet au 28 septembre 2001. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr WWW: http://www.di.ens.fr/~cousot/annonceseminaire.html *********************************************************************