********************************************************************* * 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 juin 1996 **** 14h00 ********************************* On the service Specification within a formal framework Dominique MERY (Nancy, IUF) Re'sume' : The quality of telephone services can be improved by using formal specification techniques. Temporal logic is a very expressive framework that is helpful for describing service features and for solving feature interaction problems. This paper presents a specification of services using $TLA^{+}$ as the specification language and shows how feature interactions may be detected between services. Many formal techniques have been used to deal with the general problem of service specification and one of the most exciting question on these problems is to solve the question of the interaction feature. Although formal techniques have dealt with the safety properties, we will show that the question of liveness and especially fairness are critical in the current and future intelligent network. However, many questions need to be addressed and natural language does not help in the stating in a clear and sound way the different notions such as service, feature, interaction \ldots. *** Vendredi 14 juin 1996 **** 14h00 ******************************** Relache *** Mercredi 19 juin 1996 **** Salle W **** 14h00 ******************* ------ Self-Certified Code Peter LEE (Carnegie Mellon University) Re'sume' : It is well known that it is easier to check a proof than to generate one. In this talk, I describe a mechanism called Self-Certified Code that makes use of this fact to construct efficient native-code binaries that have easily checkable properties. To make this concrete, I will give an overview of the principles and then show several examples, including a suite of network packet filters. These packet filters are extremely fast, and are unique in that they run safely in an OSF/1 operating-system kernel despite being written in hand-tuned DEC Alpha assembly language. The possibilities for distributed applications, as well as in web-computing systems such as Java, are intriguing. Self-certified code requires that the programmer somehow come up with a proof (encoded in a logical framework) of a set of safety properties. The main practical difficulty is how to do this. I will describe an assembler that we have implemented that does this automatically for network packet filters, and will also discuss its limitations. Finally, I will conclude with prospects for future work. *** Vendredi 21 juin 1996 **** 14h00 ******************************** Relache (MOVEP'96, Nantes) *** Vendredi 28 juin 1996 **** 14h00 ******************************** Rela^che (LOMAPS meeting) ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr WWW: http://www.ens.fr/~cousot/annonceseminaire.html *********************************************************************