From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 71C5C7EE25 for ; Thu, 24 Oct 2013 19:19:22 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of francois.pessaux@ensta-paristech.fr) identity=pra; client-ip=147.250.10.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="francois.pessaux@ensta-paristech.fr"; x-sender="francois.pessaux@ensta-paristech.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of francois.pessaux@ensta-paristech.fr designates 147.250.10.4 as permitted sender) identity=mailfrom; client-ip=147.250.10.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="francois.pessaux@ensta-paristech.fr"; x-sender="francois.pessaux@ensta-paristech.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of postmaster@ns4.ensta.fr designates 147.250.10.4 as permitted sender) identity=helo; client-ip=147.250.10.4; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="francois.pessaux@ensta-paristech.fr"; x-sender="postmaster@ns4.ensta.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArkBAGpVaVKT+goEnGdsb2JhbABZFoMpVL5YgR0WDgEBAQEBCAsJCRQogiwdSyMBMXQCBBOIBwQJmHCVLIwvjgQKgQs7hCwDlCqDYJNtgUCBZgkXIg X-IPAS-Result: ArkBAGpVaVKT+goEnGdsb2JhbABZFoMpVL5YgR0WDgEBAQEBCAsJCRQogiwdSyMBMXQCBBOIBwQJmHCVLIwvjgQKgQs7hCwDlCqDYJNtgUCBZgkXIg X-IronPort-AV: E=Sophos;i="4.93,563,1378850400"; d="scan'208";a="38651527" Received: from ns4.ensta.fr ([147.250.10.4]) by mail2-smtp-roc.national.inria.fr with ESMTP; 24 Oct 2013 19:19:16 +0200 Received: from ns4.ensta.fr (localhost [127.0.0.1]) by ns4.ensta.fr (Postfix) with ESMTP id BCFBDBEA9E for ; Thu, 24 Oct 2013 19:19:21 +0200 (CEST) X-Virus-Scanned: amavisd-new at ns4.ensta.fr Received: from ns4.ensta.fr ([127.0.0.1]) by ns4.ensta.fr (ns4.ensta.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 0vW2QUxF4mKz for ; Thu, 24 Oct 2013 19:19:17 +0200 (CEST) Received: from zemail.ensta.fr (zemail.ensta.fr [147.250.1.16]) by ns4.ensta.fr (Postfix) with ESMTP id 3BBBBBEA83 for ; Thu, 24 Oct 2013 19:19:17 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by zemail.ensta.fr (Postfix) with ESMTP id 2B1C32405CD1 for ; Thu, 24 Oct 2013 19:19:17 +0200 (CEST) Received: from zemail.ensta.fr ([127.0.0.1]) by localhost (zemail.ensta.fr [127.0.0.1]) (amavisd-new, port 10032) with ESMTP id cVOGPU5cUZF0 for ; Thu, 24 Oct 2013 19:19:16 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by zemail.ensta.fr (Postfix) with ESMTP id B675D240C358 for ; Thu, 24 Oct 2013 19:19:16 +0200 (CEST) X-Virus-Scanned: amavisd-new at zemail.ensta.fr Received: from zemail.ensta.fr ([127.0.0.1]) by localhost (zemail.ensta.fr [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id 1PyWrcFbDkW8 for ; Thu, 24 Oct 2013 19:19:16 +0200 (CEST) Received: from zemail.ensta.fr (localhost [127.0.0.1]) by zemail.ensta.fr (Postfix) with ESMTP id 9F8BA2405CD1 for ; Thu, 24 Oct 2013 19:19:16 +0200 (CEST) Date: Thu, 24 Oct 2013 19:19:16 +0200 (CEST) From: =?iso-8859-15?Q?Fran=E7ois?= Pessaux To: caml-list Message-ID: <75996938.5337849.1382635156583.JavaMail.zimbra@ensta.fr> In-Reply-To: <1017308589.5337391.1382634964587.JavaMail.zimbra@ensta.fr> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-15 Content-Transfer-Encoding: quoted-printable X-Originating-IP: [31.33.148.170] X-Mailer: Zimbra 8.0.4_GA_5739 (ZimbraWebClient - SAF7 (Mac)/8.0.4_GA_5737) Thread-Topic: First International Workshop on Formal Integrated Development Environment. Thread-Index: UTreyaNaBCU2Kwnfcvm97bzymB9jlA== Subject: [Caml-list] [CFP] First International Workshop on Formal Integrated Development Environment. [Please post - apologies for multiple copies.] First Call for Papers - F-IDE 2014 - First International Workshop on Formal Integrated Development Environment= =20 (Satellite event of ETAPS) April 6th, 2014, Grenoble, France http://www.ensta-paristech.fr/~etaps/ WORKSHOP AIM High levels of safety, security and also privacy standards require the use = of formal methods to specify and develop compliant software (sub)systems= . Any standard comes with an assessment process, which requires a complete= documentation of the application in order to ease the justification of de= sign choices and the review of code and proofs. Ideally, an F-IDE dedicated to such developments should comply with severa= l requirements. The first one is to associate a logical theory with a progr= amming language, in a way that facilitates the tightly coupled handling o= f specification properties and program constructs. The second one is to o= ffer a language/environment simple enough to be usable by most developers,= even if they are not fully acquainted with higher-order logics or set theo= ry, in particular by making development of proofs as easy as possible. Th= e third one is to offer automated management of application documentation. = It may also be expected that developments done with such an F-IDE are reu= sable and modular. Moreover, tools for testing and static analysis may be = embedded in this F-IDE, to help address most steps of the assessment proce= ss. TOPICS We encourage submissions presenting and discussing research efforts as well= as experience returns on design, development, usage of tools aiming at mak= ing formal methods "easier" for non-specialists.=20 In this context, the topics include (but are not limited to): - F-IDE building : design and integration of languages, compilation - How to make high-level logical and programming concepts palatable to indu= strial developers - Integration of Object-Oriented and modularity features - Integration of static analysers - Integration of automatic proof tools, theorem provers and testing tools - Documentation tools - Impact of tools on certification - Experience reports of developing F-IDE - Experience reports of using F-IDE - Experience reports of formal methods-based assessments of industrial app= lications We encourage not only mature research results, submissions presenting=20 innovative ideas and early results are also of interest. SUBMISSIONS Papers (6-14 pages in length), following EPCTS format are expected. They = can be: * Research papers providing new concepts and results * Position papers and research perspectives * Experience reports * Tool presentations Submissions will be done via Easychair: https://www.easychair.org/conferenc= es/?conf=3Dfide2014 PROCEEDINGS Final versions of accepted papers will be published in a volume of the Elec= tronic Proceedings in Theoretical Computer Science (EPTCS). IMPORTANT DATES * Abstract submission : 18 December, 2013 * Paper Submission : 23 December, 2013 * Notification : 27 January, 2014 * Final version : 10 February, 2014 * Workshop date: April 6, 2014 PC CO-CHAIRS * Catherine Dubois, CNAM - C=E9dric / ENSIIE, (at) ensiie (d= ot) fr * Dimitra Giannakopoulou, NASA Ames, (dot) (at)= nasa (dot) gov * Dominique Mery, LORIA / Universit=E9 de Lorraine, (dot) <= last name> (at) loria (dot) fr Best regards, -- Fran=E7ois PESSAUX Enseignant-chercheur ENSTA ParisTech Unit=E9 d'Informatique et d'Ing=E9nierie des Syst=E8mes Bureau : R328 828 boulevard des Mar=E9chaux, 91120 Palaiseau T=E9l: 01 81 87 20 73 Email: francois.pessaux@ensta-paristech.fr