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=1.4 required=5.0 tests=AWL,HTML_MESSAGE, SUBJECT_ENCODED_TWICE autolearn=disabled version=3.1.3 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 4836BBB84 for ; Wed, 8 Oct 2008 10:45:42 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnIDAHMQ7EjAXQIniGdsb2JhbACCc5BvAQEBFSKqQoFq X-IronPort-AV: E=Sophos;i="4.33,377,1220220000"; d="scan'208,217";a="30027737" Received: from concorde.inria.fr ([192.93.2.39]) by mail4-smtp-sop.national.inria.fr with ESMTP; 08 Oct 2008 10:45:41 +0200 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m988jG5x018657 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Wed, 8 Oct 2008 10:45:41 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApEDAHQP7EjUGyoegWdsb2JhbACCc5BvAQEWIgOqNoFq X-IronPort-AV: E=Sophos;i="4.33,377,1220220000"; d="scan'208,217";a="17785614" Received: from smtp4-g19.free.fr ([212.27.42.30]) by mail3-smtp-sop.national.inria.fr with ESMTP; 08 Oct 2008 10:45:40 +0200 Received: from smtp4-g19.free.fr (localhost.localdomain [127.0.0.1]) by smtp4-g19.free.fr (Postfix) with ESMTP id 79DD83EA122 for ; Wed, 8 Oct 2008 10:45:40 +0200 (CEST) Received: from [192.168.0.2] (sgc91-2-82-237-76-251.fbx.proxad.net [82.237.76.251]) by smtp4-g19.free.fr (Postfix) with ESMTP id 1EE493EA138 for ; Wed, 8 Oct 2008 10:45:40 +0200 (CEST) Mime-Version: 1.0 (Apple Message framework v753.1) To: caml-list@inria.fr Message-Id: <51F214F9-D7D6-4A17-A9A2-85FD708B024C@ensiie.fr> Content-Type: multipart/alternative; boundary=Apple-Mail-3-335201798 From: Sandrine Blazy Subject: =?ISO-8859-1?Q?TSI_num=E9ro_sp=E9cial_ANALYSE_STATIQUE_et_COMPIL?= =?ISO-8859-1?Q?ATION_=282e_appel=29?= Date: Wed, 8 Oct 2008 10:45:37 +0200 X-Mailer: Apple Mail (2.753.1) X-Miltered: at concorde with ID 48EC731C.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; compil:01 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 --Apple-Mail-3-335201798 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed [Veuillez nous excusez pour les r=E9ceptions multiples =E9ventuelles. N'h=E9sitez pas =E0 diffuser largement cet appel.] Technique et Science Informatiques (TSI) 2e 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: 30 novembre 2008 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://=20= tsi.e-revues.com/appel.jsp). Les articles peuvent appara=EEtre dans 3 rubriques : article de =20 recherche (entre 22 et 26 pages), de synth=E8se (jusqu'=E0 30 pages) ou =20= 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 apres envoi, nous vous demandons de nous contacter =20 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-3-335201798 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=ISO-8859-1
[Veuillez nous excusez pour les r=E9ceptions multiples = =E9ventuelles.
N'h=E9sitez pas =E0 diffuser = largement cet appel.]
=A0=A0 =A0 =A0 =A0 =A0 =A0 =A0= =A0 =A0 =A0Technique et Science Informatiques (TSI)

=A0=A0 =A0 = =A0 =A0 =A0 =A0 =A0 =A02e appel =E0 propositions d'articles sur le = th=E8me

=A0=A0 =A0 =A0 =A0 =A0 =A0 =A0APPLICATION DES M=C9THODES= FORMELLES =C0=A0
=A0=A0 =A0 = =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 =A0 =A0 =A0 =A0 =A0 =A0 = Date limite de soumission: 30 novembre 2008

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 soumission usuelles de la revue TSI = (voir http://tsi.e-revues.com/appel.j= sp).=A0
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).=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 apres 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-3-335201798--