********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle W, 4e`me e'tage, toits du DMA * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 3 mars 2000 **** 14h00 ********************************* Witold CHARATONIK (Max-Planck-Institut f"ur Informatik, Saarbr"ucken) Directional types for logic programs Re'sume': Directional types form a type system for logic programs which is based on the view of a predicate as a directional procedure which, when applied to a tuple of input terms, generates a tuple of output terms. It is known that directional-type checking wrt. arbitrary types is undecidable; Aiken and Lakshman proved the decidability of the problem wrt. discriminative regular types. In this talk, we characterize directional types in model-theoretic terms. We present an algorithm for inferring directional types. The directional type that we derive from a logic program P is uniformly at least as precise as any discriminative directional type of P, i.e., any directional type out of the class for which the type checking algorithm of Aiken and Lakshman is sound and complete. Moreover, using techniques based on tree automata, we show that directional-type checking for logic programs wrt. general regular types is decidable, DEXPTIME-complete and fixed-parameter linear. The last result shows that despite the exponential lower bound, the type system might be usable in practice. *** Lundi 13 mars 2000 **** 9h00--17h00 *** Salle Dussane *********** ----- ----------- ------------- Noter la date, l'horaire et le lieu exceptionnels. Pour des raisons d'organisation, veuillez pre'venir Joelle.Isnard@ens.fr de votre pre'sence avant le 10 mars 2000. ********************************************************************* Se'minaire << O`u me`ne l'interpre'tation abstraite ? ********************************************************************* 9h00--9h30 : Je'ro^me Feret (ENS), Analyse de la confidentialite' des syste`mes mobiles ; 9h30--10h00 : David Monniaux (ENS), Interpre'tation abstraite probabiliste ; 10h00--10h30 : Bruno Blanchet (INRIA) Analyses d'e'chappement pour les langages objets, application a` Java ; 11h00--11h30 : Franck Ve'drine (ENS), Analyses totales par interpre'tation abstraite ; 11h30--12h00 : Laurent Mauborgne (ENS), Repre'sentation d'ensembles d'arbres pour l'interpre'tation abstraite ; 12h00--12h30 : E'ric Goubault (CEA-LETI) Quelques proble`mes de se' mantiques pour l'analyse statique ; 14h00--14h30 : Jean Goubault-Larrecq (GIE Dyade & projet Coq, INRIA) Une me'thode automatique de ve'rification de protocoles cryptographiques ; 14h00--14h30 : Franc,ois Bourdoncle (ENSMP) Le futur de la recherche d'informations sur Internet ; 14h30--15h00 : Alain Deutsch (PolySpace Technologies) Interpre'tation abstraite et algorithmique: de l'exponentiel au sous-polynomial ; 15h30--16h00 : Nicolas Mercouroff (Alcatel) De l'interpre'tation abstraite aux te'le'communications ; 16h30--17h00 : Dominique Me'ry (LORIA & UHP, IUF) Analyse des interactions de services par abstraction et par affinement ; 17h00--17h30 : Patrick Cousot (ENS) Perspectives pour l'interpre'tation abstraite. *** Vendredi 10 mars 2000 **** 14h00 ******************************** Changement de salle : salle Verdier, Passage vert, 1er etage. ********************************************************************* Andreas Podelski (Max-Planck-Institut f"ur Informatik) Model Checking and Solved Forms Re'sume' : The model checking procedures for the two cases of systems (1) over stacks or other symbolic data and (2) over integers or reals, seem incomparable in existing presentations. We show how one can formalize these procedures as one generic constraint-solving procedure, viz. the transformation of a second-order constraint into an equivalent constraint in solved form. The solved form is (1) a recursive resp. (2) a non-recursive definition of the set of states satisfying the given temporal property. *** Vendredi 17 mars 2000 **** 14h00 ********************************* Andreas Podelski (Max-Planck-Institut f"ur Informatik) Static Analysis of Array Bounds as Infinite-State Model Checking Re'sume': Steffen, Schmidt and most recently Cousot and Cousot established a connection between dataflow analysis and finite-state model checking. This connection continues to hold in the infinite-state case. We only need to realize that infinite-state model checking is often a form of data flow analysis applied to flow graphs with nodes labeled by arithmetic constraints. This leads us reuse the by now practical technology for the verification of integer-valued protocols or real-time and hybrid systems for the static analysis of C programs. We present a system that automatically derives (exact or conservatively approximated) weakest preconditions on procedure parameters for the well-definedness of array operations, or for other execution properties. This enables a form of `abstract debugging' `a la Bourdoncle or a potential help with annotations in the `Extended Static Checking' approach of Detlevs, Leino, Nelson and Saxe. *** Vendredi 24 mars 2000 **** 15h00 ******************************** ^^^^^ Tomas E. Uribe (CS, Stanford University) Extended Finite-State Abstractions Re'sume': Many verification methods explicitly or implicitly construct finite-state system abstractions, which are explicitly or implicitly model checked. We show how such abstractions can be represented, combined and model checked in a general way. For this, we define a class of extended finite-state abstractions and present an algorithmic model checking procedure for them. Besides a standard \forallCTL*-preserving safety component, the extended abstractions include extra bounds on fair transitions, well-founded orders, and constrained transition relations for checking existential properties and the generation of LTL counterexamples. This approach minimizes the need for user interaction and maximizes the impact of the available automated deduction and model checking tools. *** Vendredi 31 mars 2000 **** 14h00 ******************************** rela^che ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************