From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: ** X-Spam-Status: No, score=2.4 required=5.0 tests=AWL,HTML_MESSAGE,SPF_SOFTFAIL, SUBJECT_ENCODED_TWICE autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id AE211BBAF for ; Tue, 2 Dec 2008 18:18:35 +0100 (CET) X-IronPort-AV: E=Sophos;i="4.33,702,1220220000"; d="scan'208,217";a="17886019" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 02 Dec 2008 18:18:35 +0100 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id mB2HIZf4032737 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Tue, 2 Dec 2008 18:18:35 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtkAANj8NEnUGyodkWdsb2JhbACCRCyQXQEBAQEJCwoHEQO+YIJ/ X-IronPort-AV: E=Sophos;i="4.33,702,1220220000"; d="scan'208,217";a="17886017" Received: from smtp3-g19.free.fr ([212.27.42.29]) by mail2-smtp-roc.national.inria.fr with ESMTP; 02 Dec 2008 18:18:34 +0100 Received: from smtp3-g19.free.fr (localhost.localdomain [127.0.0.1]) by smtp3-g19.free.fr (Postfix) with ESMTP id AA1D117B987 for ; Tue, 2 Dec 2008 18:18:34 +0100 (CET) Received: from [192.168.0.2] (sgc91-2-82-237-76-251.fbx.proxad.net [82.237.76.251]) by smtp3-g19.free.fr (Postfix) with ESMTP id 4D20717B985 for ; Tue, 2 Dec 2008 18:18:34 +0100 (CET) Mime-Version: 1.0 (Apple Message framework v753.1) To: caml-list@inria.fr Message-Id: <1A5A7B64-DD0E-485B-A055-ABD27B955E25@ensiie.fr> Content-Type: multipart/alternative; boundary=Apple-Mail-27-823008176 From: Sandrine Blazy Subject: =?ISO-8859-1?Q?TSI_num=E9rosp=E9cial_ANALYSE_STATIQUE_et_COMPILA?= =?ISO-8859-1?Q?TION:_extension_des_envois_au_15_f=E9vrier?= Date: Tue, 2 Dec 2008 18:18:31 +0100 X-Mailer: Apple Mail (2.753.1) X-Miltered: at concorde with ID 49356DEB.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; compilation:01 evry:01 statiques:01 compilateurs:01 specifier:01 envisageable:01 compilateur:01 statiques:01 compilation:01 semantique:01 formelle:01 abstraite:01 formalismes:01 logiques:01 formelle:01 --Apple-Mail-27-823008176 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed [Veuillez nous excuser pour les r=E9ceptions multiples =E9ventuelles. N'h=E9sitez pas =E0 diffuser largement cet appel.] Extension de la date limite de soumission au ************** 15 f=E9vrier 2009 **************** ------------------------------------------------------------------------=20= ---------------- Technique et Science Informatiques (TSI) Appel =E0 propositions d'articles sur le th=E8me APPLICATION DES M=C9THODES FORMELLES =C0 L'ANALYSE STATIQUE ET LA COMPILATION Coordonateur: Sandrine Blazy (ENSIIE, laboratoire CEDRIC, =C9vry) Date limite de soumission: 15 f=E9vrier 2009 Ce num=E9ro sp=E9cial vise =E0 faire le point sur les travaux de = recherche =20 et les techniques fond=E9s sur les m=E9thodes formelles am=E9liorant la = conception =20 s=FBre d'analyses statiques et de compilateurs. Les m=E9thodes formelles permettent de sp=E9cifier des syst=E8mes de = plus =20 en plus complexes. Il est d=E9sormais envisageable de v=E9rifier formellement un compilateur optimisant et r=E9aliste, ou encore de concevoir des = analyses statiques enti=E8rement automatiques. Ceci est rendu possible gr=E2ce =E0 = des progr=E8s r=E9cents accomplis dans diff=E9rents domaines utilis=E9s par =20= l'analyse statique et la compilation. Citons par exemple la s=E9mantique formelle =20= des langages de programmation, les mod=E8les de m=E9moire pour la = concurrence, l'interpr=E9tation abstraite, les formalismes logiques pour la preuve de programmes, la m=E9canisation du raisonnement dans les assistants =E0 la preuve. L'objectif de ce num=E9ro th=E9matique est de faire le point des travaux = =20 dans le domaine de la conception formelle d'analyses statiques et de =20 compilateurs, en abordant notamment les th=E8mes suivants: interpr=E9tation abstraite, domaines abstraits, analyses de pointeurs, d=E9tection de bogues, analyses fond=E9es sur les types, application des techniques de programmation par contraintes, analyse de flot d'information, compilateurs pour langages sp=E9cialis=E9s, compilateurs pour langages synchrones, compilateurs pour syst=E8mes h=E9t=E9rog=E8nes distribu=E9s, compilation =E0 la vol=E9e, interaction entre compilateur et architecture, validation de traducteurs, code auto-certifi=E9, gestion de la m=E9moire, optimisations de programmes, v=E9rification logique de programmes, ... . Soumission. TSI est une revue francophone; les articles doivent =EAtre r=E9dig=E9s = en fran=E7ais sauf si _aucun_ des auteurs n'est francophone. Les articles seront lus par deux lecteurs de la r=E9daction de TSI et deux membres du comit=E9 de lecture. Les d=E9cisions seront prises sur la base de leurs avis et des = discussions qui en d=E9couleront. Les propositions d'articles devront respecter les r=E8gles de =20 pr=E9sentation et de soumission usuelles de la revue TSI (voir http://tsi.e-revues.com/=20 appel.jsp). Les articles peuvent appara=EEtre dans 3 rubriques : article de = recherche (entre 22 et 26 pages), de synth=E8se (jusqu'=E0 30 pages) ou = d'application (jusqu'=E0 20 pages). La soumission se fait par envoi de l'article, au format PDF, par =20 courrier =E9lectronique =E0 Laurence Sourdillon - sourdillon@lavoisier.fr Si vous ne recevez pas de message confirmant sa bonne r=E9ception moins =20= d'une semaine apr=E8s envoi, nous vous demandons de nous contacter = directement. Comit=E9 de lecture: - Yves Bertot, INRIA Sophia-Antipolis M=E9diterran=E9e - Sandrine Blazy, ENSIIE, =C9vry - Arnaud Gotlieb, INRIA, Rennes - Bretagne Atlantique - Bertrand Jeannet, INRIA Rh=F4ne-Alpes, Grenoble - Benjamin Monate, CEA LIST, Saclay - Pierre-Etienne Moreau, INRIA Nancy - Grand Est - Dillon Pariente, Dassault Aviation, Saint-Cloud - Marc Pouzet, Universit=E9 Paris-Sud, Orsay - Xavier Rival, ENS, Paris - Nadia Tawbi, Universit=E9 Laval, Canada --Apple-Mail-27-823008176 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=ISO-8859-1
[Veuillez nous excuser pour les r=E9ceptions multiples = =E9ventuelles.
N'h=E9sitez pas =E0 diffuser = largement cet appel.]

Extension de la date limite de soumission = au
************** 15 f=E9vrier = 2009 =A0 ****************

---------------------------------------------------------------= -------------------------
=A0=A0 =A0 = =A0 =A0 =A0 =A0Technique et Science Informatiques (TSI)

=A0=A0 =A0 = =A0 =A0 =A0Appel =E0 propositions d'articles sur le = th=E8me

=A0=A0 =A0 =A0 APPLICATION DES M=C9THODES FORMELLES = =C0=A0
=A0=A0 =A0 =A0 =A0 L'ANALYSE = STATIQUE ET LA COMPILATION

=A0 =A0 Coordonateur: Sandrine Blazy (ENSIIE, = laboratoire CEDRIC, =C9vry)

=A0=A0 =A0 =A0 =A0 =A0 =A0 =A0=A0Date limite de = soumission: 15 f=E9vrier 2009

Ce num=E9ro sp=E9cial vise =E0 faire le point sur les = travaux de recherche et les
techniques fond=E9s sur les m=E9thodes formelles am=E9liorant = la conception s=FBre
d'analyses statiques et de compilateurs.

Les = m=E9thodes formelles permettent de sp=E9cifier des syst=E8mes de plus en = plus
complexes. Il est d=E9sormais = envisageable de v=E9rifier formellement un=A0
compilateur optimisant et r=E9aliste, ou encore de = concevoir des analyses=A0
statiques = enti=E8rement automatiques. Ceci est rendu possible gr=E2ce =E0 = des=A0
progr=E8s r=E9cents = accomplis dans diff=E9rents domaines utilis=E9s par = l'analyse=A0
statique et la compilation. = Citons par exemple la s=E9mantique formelle des=A0
langages de programmation, les mod=E8les de m=E9moire = pour la concurrence,=A0
l'interpr=E9tation abstraite, les formalismes logiques pour = la preuve de=A0
programmes, la m=E9canisation = du raisonnement dans les assistants =E0 la=A0
preuve.

L'objectif de ce num=E9ro th=E9matique est de faire le = point des travaux=A0 dans le=A0
domaine = de la conception formelle d'analyses statiques et de compilateurs, = en
abordant notamment les = th=E8mes suivants:
  • interpr=E9tation abstraite,
  • domaines abstraits,
  • analyses de = pointeurs,
  • d=E9tection de bogues,
  • analyses fond=E9es sur les types,
=
  • application des techniques de programmation par = contraintes,
  • analyse de flot d'information,
  • compilateurs pour langages = sp=E9cialis=E9s,
  • compilateurs pour langages synchrones,
  • compilateurs pour syst=E8mes = h=E9t=E9rog=E8nes distribu=E9s,
  • compilation =E0 la vol=E9e,
  • interaction entre = compilateur et architecture,
  • validation de traducteurs,
  • code = auto-certifi=E9,
  • gestion de la m=E9moire,=A0
  • optimisations de = programmes,
  • v=E9rification logique de programmes,
  • ... .

Soumission.

TSI est une revue francophone; les articles doivent = =EAtre r=E9dig=E9s en
fran=E7ais = sauf si _aucun_ des auteurs n'est francophone.
Les articles seront lus par deux lecteurs de la = r=E9daction de TSI et
deux = membres du comit=E9 de lecture.
Les = d=E9cisions seront prises sur la base de leurs avis et des = discussions
qui en = d=E9couleront.

Les propositions d'articles devront respecter les = r=E8gles de pr=E9sentation et de=A0
soumission usuelles de la revue TSI (voir http://tsi.e-revues.com/appel.jsp).=A0
Les articles peuvent appara=EEtre dans = 3 rubriques : article de recherche=A0
(entre 22 et 26 pages), de synth=E8se (jusqu'=E0 30 = pages) ou d'application=A0
(jusqu'=E0 = 20 pages).=A0

La soumission se fait par envoi de l'article, au = format PDF, par courrier
=E9lectronique =E0 Laurence Sourdillon=A0 - sourdillon@lavoisier.fr
Si vous ne recevez pas de message confirmant sa bonne = r=E9ception moins d'une
semaine = apr=E8s envoi, nous vous demandons de nous contacter = directement.

Comit=E9 de lecture:
- Yves Bertot, INRIA Sophia-Antipolis = M=E9diterran=E9e=A0
- = Sandrine Blazy, ENSIIE, =C9vry
- Arnaud = Gotlieb, INRIA, Rennes - Bretagne Atlantique
- Bertrand Jeannet, INRIA Rh=F4ne-Alpes, = Grenoble
- Benjamin Monate, CEA LIST, = Saclay
- Pierre-Etienne Moreau, = INRIA Nancy - Grand Est
- Dillon = Pariente, Dassault Aviation, Saint-Cloud
- Marc Pouzet, Universit=E9 Paris-Sud, = Orsay
- Xavier Rival, ENS, = Paris
- Nadia Tawbi, Universit=E9 = Laval, Canada


= --Apple-Mail-27-823008176--