********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle U/V, etage -2 * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 6 fevrier 2004 **** 14h00 ****************************** David SCHMIDT (Kansas State University & Ecole polytechnique) Closed and Logical Relations for Over- and Under-approximation of Powersets Re'sume' : We apply lower and upper powerset constructions to abstract interpretation, in particular, to formalizing the mixed-transition systems of Dams. To aid our study, we formalize Galois connections as Upper-Lower-GLB-LUB-closed binary relations, and we define a family of logical relations for generating Galois connections. Our results are (1) Unlike the relational forms of the standard type constructors, x and ->, the constructors for the lower and upper powersets do not necessarily generate Galois connections from their arguments, so we give sufficient conditions for doing so. (2) We prove that Dams's simulation-based, most-precise over- and under-approximations of a transition relation can be formulated classically, in terms of Galois connections on lower and upper powersets. The under-approximation construction is interesting because it embeds an upper powserset within a lower powerset. (3) We extract from the family of logical relations a validation logic that is a subset of Hennessy-Milner (and description) logic, and we obtain an easy proof of soundness. We also extract a sound refutation logic --- this gives a classical foundation to ``three-valued'' analysis systems like TVLA. *** Vendredi 13 fevrier 2004 **** 14h00 ****************************** Isabelle POLLET (UCL, Louvain-la-Neuve) Towards a generic framework for the abstract interpretation of Java Re'sum'e : The application field of static analysis techniques for object-oriented programming is getting broader, ranging from compiler optimizations to verification issues. Therefore, a generic framework easily adaptable to various kinds of analyses is useful to minimize the correctness proof effort. We discuss the foundations of a framework aimed at defining and implementing a `generic' Java code analyzer, based on the Abstract Interpretation methodology. The analysis is limited to a representative subset of Java, without concurrency. The framework is composed of a family of abstract domains, a `generic' abstract semantics based on these domains and a post-fixpoint algorithm to compute this semantics. We also developed a complete implementation of the framework. In the talk, we explain the different components of the framework, especially the abstract semantics. We present some results of the analyzer in order to illustrate its strengths and weaknesses. We suggest some improvements that will be soon investigated. *** Vendredi 20 fevrier 2004 **** 9h00 --18h00 ********************* Se'minaire d'une journee sur la securite, voir le programme en : http://www.di.ens.fr/~cousot/seminaire/2004/seminaire.securite-04-02-fev.txt *** Vendredi 27 fevrier 2004 **** 14h00 ***************************** Francesco TAPPARO (Universita`degli Studi di Podava & Ecole polytechnique Completeness in abstract interpretation, bisimulation and strongly preserving abstract model checking Re'sume' : In this seminar we will present our results about the relationship between complete abstract interpretation and strongly preserving abstract model checking. Completeness is a well established property for an abstract interpretation; it means that no loss of information happens in the abstract computation relatively to the semantic properties encoded by the abstraction. Abstract model checking is a well known technique used to check models. Selected properties of the model states are approximated, giving thus rise to an abstract and simpler model. Preservation theorems guarantee that a property true in the abstract remains true in the concrete model. When the opposite inference is possible, namely when a property false in the abstract is false in the concrete, the abstract model is said strongly preserving. Classically algorithms refining transition systems in order to get strong preservation compute a state equivalence. This is restrictive because, in a generic abstract interpretation-based view, state equivalences are just one particular type of abstraction. We proved that the problem of minimally refining an abstract model checking in order to get strong preservation can be formulated as a complete shell in abstract interpretation. As a consequence of these results, we show that some well-known behavioural equivalences used in process algebra like simulation and bisimulation can be elegantly characterized in pure abstract interpretation as completeness properties. With this approach it is possible to develop refinement algorithms for generic languages, exploiting standard refinement algorithms. ********************************************************************* Pour recevoir l'annonce par courrier electronique: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************