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 D841B7FC41; Wed, 4 Mar 2015 10:23:01 +0100 (CET) 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: A0DRAgBMzvZUnAQK+pNaFoM+g2W+MQEJgXSDfCqBAE0BAQEBAQEQAQEBAQEIFAkuFIQHLAZFbgKGY4I+Da0Tj0iaRAEBAQEdjE+CWQRQgjgMLw8DHYEUBYRogQiNaYIYij+EB4hpAoIygWBvgQGBQQEBBQ X-IPAS-Result: A0DRAgBMzvZUnAQK+pNaFoM+g2W+MQEJgXSDfCqBAE0BAQEBAQEQAQEBAQEIFAkuFIQHLAZFbgKGY4I+Da0Tj0iaRAEBAQEdjE+CWQRQgjgMLw8DHYEUBYRogQiNaYIYij+EB4hpAoIygWBvgQGBQQEBBQ X-IronPort-AV: E=Sophos;i="5.09,686,1418079600"; d="scan'208,217";a="124303496" Received: from ns4.ensta.fr ([147.250.10.4]) by mail2-smtp-roc.national.inria.fr with ESMTP; 04 Mar 2015 10:23:01 +0100 Received: from ns4.ensta.fr (localhost [127.0.0.1]) by ns4.ensta.fr (Postfix) with ESMTP id 41B84E091A; Wed, 4 Mar 2015 10:23:01 +0100 (CET) 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 yMtBxEZ7Eu8d; Wed, 4 Mar 2015 10:23:00 +0100 (CET) Received: from zemail.ensta.fr (zemail.ensta.fr [147.250.1.16]) by ns4.ensta.fr (Postfix) with ESMTP id 6DD10E090E; Wed, 4 Mar 2015 10:23:00 +0100 (CET) Received: from localhost (localhost [127.0.0.1]) by zemail.ensta.fr (Postfix) with ESMTP id 67CD9297203; Wed, 4 Mar 2015 10:23:00 +0100 (CET) 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 pSBh08iZp0hF; Wed, 4 Mar 2015 10:22:59 +0100 (CET) Received: from localhost (localhost [127.0.0.1]) by zemail.ensta.fr (Postfix) with ESMTP id 6EC6D297202; Wed, 4 Mar 2015 10:22:59 +0100 (CET) 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 ZbVBRSW9I1A4; Wed, 4 Mar 2015 10:22:59 +0100 (CET) Received: from [147.250.222.190] (unknown [147.250.222.190]) by zemail.ensta.fr (Postfix) with ESMTPSA id 4A0C4297203; Wed, 4 Mar 2015 10:22:59 +0100 (CET) From: =?utf-8?Q?Fran=C3=A7ois_Pessaux?= Content-Type: multipart/alternative; boundary="Apple-Mail=_CD9C4CF8-0B76-4B60-8E4A-07676A5C6684" Date: Wed, 4 Mar 2015 10:22:58 +0100 Message-Id: Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2070.6\)) X-Mailer: Apple Mail (2.2070.6) Subject: [Caml-list] [CFP] F-IDE 2015 --Apple-Mail=_CD9C4CF8-0B76-4B60-8E4A-07676A5C6684 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Dear all, Sorry if you get multiple copies. Regards, =E2=80=94 Fran=C3=A7ois ****************************************************************** F-IDE 2015 - CALL FOR PAPERS ****************************************************************** The 2nd Formal Integrated Development Environment Workshop (F-IDE 2015) 22 June 2015, Oslo, Norway http://www.eecs.qmul.ac.uk/~masci/fide2015 ****************************************************************** -------- OVERVIEW -------- The 2nd Formal Integrated Development Environment Workshop (F-IDE 2015) wil= l be held in Oslo, Norway, in June, 2015. High levels of safety, security and also privacy standards require the use = of formal methods to specify and develop compliant software (sub)systems. A= ny standard comes with an assessment process, which requires a complete doc= umentation of the application in order to ease the justification of design = choices and the review of code and proofs. Ideally, an F-IDE dedicated to such developments should comply with several= requirements. The first one is to associate a logical theory with a progra= mming language, in a way that facilitates the tightly coupled handling of s= pecification properties and program constructs. The second one is to offer = a language/environment simple enough to be usable by most developers, even = if they are not fully acquainted with higher-order logics or set theory, in= particular by making development of proofs as easy as possible. The third = one is to offer automated management of application documentation. It may a= lso be expected that developments done with such an F-IDE are reusable and = modular. Moreover, tools for testing and static analysis may be embedded in= this F-IDE, to help address most steps of the assessment process. ------ TOPICS ------ The workshop is opened to contributions on all aspects of a system developm= ent process, including specification, design, implementation, analysis and = documentation. It should allow the presentation of tools, methods, techniqu= es and experiments. Topics of interest include, but are not limited to, the= following: =E2=80=93 F-IDE building: design and integration of languages, compilation =E2=80=93 How to make high-level logical and programming concepts palatable= to industrial developers =E2=80=93 Integration of Object-Oriented and modularity features =E2=80=93 Integration of static analyzers =E2=80=93 Integration of automatic proof tools, theorem provers and testing= tools =E2=80=93 Documentation tools =E2=80=93 Impact of tools on certification =E2=80=93 Experience reports of developing F-IDE =E2=80=93 Experience reports of using F-IDE =E2=80=93 Experience reports of formal methods-based assessments of industr= ial applications ---------- SUBMISSION ---------- Papers must be written in English, not exceed 15 pages in LNCS format, not = counting references, and follow the FM 2015 Format and Submission Guideline= s. They can be: - Research papers providing new concepts and results - Position papers and research perspectives - Experience reports - Tool presentations Papers can be submitted through Easychair: https://easychair.org/conference= s/?conf=3Dfide2015 ----------- PROCEEDINGS ----------- - Preliminary proceedings, including all the papers selected for the worksh= op, will be available electronically at the workshop. - Post proceedings are under consideration as Electronic Proceedings in The= oretical Computer Science (ETPCS) proceedings. --------------- IMPORTANT DATES --------------- Abstract submission: March 24, 2015 (23h59 GMT) Paper submission: March 31, 2015 (23h59 GMT) Notification: April 30, 2015 Camera-ready: May 15, 2015 Workshop: June 22, 2015 ----------------- PC CO-CHAIRS ----------------- Catherine Dubois ENSIIE, Cedric, catherine (dot) dubois (at) ensiie (do= t) fr Paolo Masci Queen Mary University of London, paolo (dot) masci (at= ) eecs (dot) qmul (dot) ac (dot) uk Dominique Mery Universit=C3=A9 de Lorraine, dominique (dot) mery (at)= loria (dot) fr ----------------- PC MEMBERS (to be completed) ----------------- Bernhard Beckert Karlsruhe Institute of Technology Jose Campos Universidade do Minho Paul Curzon Queen Mary University of London Carlo Alberto Furia ETH Zurich Therese Hardin UPMC Rustan Leino Microsoft Research Michael Leuschel University of Dusseldorf Claude Marche INRIA Stefan Mitsch Carnegie Mellon University Patrick Oladimeji Swansea University Suzette Person NASA Langley Research Center Francois Pessaux ENSTA ParisTech Marie-Laure Potet Laboratoire Verimag Steve Reeves Waikato University John Rushby SRI International Rene Thiemann University of Innsbruck Boris Yakobowski CEA LIST --Apple-Mail=_CD9C4CF8-0B76-4B60-8E4A-07676A5C6684 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 Dear all,

Sorry if you get&nbs= p;multiple copies.
Regards,

 =E2=80=94 Fran=C3=A7ois

******************************************************************
           &= nbsp;   F-IDE 2015 - CALL FOR PAPERS
*********= *********************************************************
      The 2nd Formal Integrated D= evelopment Environment Workshop
     = ;            &n= bsp;        (F-IDE 2015)
           &nb= sp;      22 June 2015, Oslo, Norway
           http://www.e= ecs.qmul.ac.uk/~masci/fide2015

***********= *******************************************************

--------
OVERVIEW
--------
The 2nd Formal Integrated Development Environment Workshop (F-IDE 201= 5) will be held in Oslo, Norway, in June, 2015.

High levels of safety, security and also privacy standards require the us= e of formal methods to specify and develop compliant software (sub)systems.= Any standard comes with an assessment process, which requires a complete d= ocumentation of the application in order to ease the justification of desig= n choices and the review of code and proofs.

I= deally, an F-IDE dedicated to such developments should comply with several = requirements. The first one is to associate a logical theory with a program= ming language, in a way that facilitates the tightly coupled handling of sp= ecification properties and program constructs. The second one is to offer a= language/environment simple enough to be usable by most developers, even i= f they are not fully acquainted with higher-order logics or set theory, in = particular by making development of proofs as easy as possible. The third o= ne is to offer automated management of application documentation. It may al= so be expected that developments done with such an F-IDE are reusable and m= odular. Moreover, tools for testing and static analysis may be embedded in = this F-IDE, to help address most steps of the assessment process.

------
TOPICS
------
The workshop is opened to contributions on all aspects of a system= development process, including specification, design, implementation, anal= ysis and documentation. It should allow the presentation of tools, methods,= techniques and experiments. Topics of interest include, but are not limite= d to, the following:

=E2=80=93 F-IDE building:= design and integration of languages, compilation
=E2=80=93 H= ow to make high-level logical and programming concepts palatable to industr= ial developers
=E2=80=93 Integration of Object-Oriented and m= odularity features
=E2=80=93 Integration of static analyzers<= br class=3D"">=E2=80=93 Integration of automatic proof tools, theorem prove= rs and testing tools
=E2=80=93 Documentation tools
=E2=80=93 Impact of tools on certification
=E2=80=93 Ex= perience reports of developing F-IDE
=E2=80=93 Experience rep= orts of using F-IDE
=E2=80=93 Experience reports of formal me= thods-based assessments of industrial applications

----------
SUBMISSION
----------
Papers must be written in English, not exceed 15 pages in LNCS format= , not counting references, and follow the FM 2015 Format and Submission Gui= delines.

They can be:
- Research= papers providing new concepts and results
- Position papers = and research perspectives
- Experience reports
= - Tool presentations

Papers can be submitted t= hrough Easychair: https://easychair.org/conferences/?conf=3Dfide2015<= /a>


-----------
P= ROCEEDINGS
-----------
- Preliminary proceeding= s, including all the papers selected for the workshop, will be available el= ectronically at the workshop.
- Post proceedings are under co= nsideration as Electronic Proceedings in Theoretical Computer Science (ETPC= S) proceedings.

---------------
= IMPORTANT DATES
---------------
Abstract submis= sion:  March 24, 2015 (23h59 GMT)
Paper submission: &nbs= p;   March 31, 2015 (23h59 GMT)
Notification: =         April 30, 2015
Camera-ready:         May 15, 201= 5
Workshop:         &= nbsp;   June 22, 2015

---------= --------
PC CO-CHAIRS
-----------------
Catherine Dubois     ENSIIE, Cedric, catherine (= dot) dubois (at) ensiie (dot) fr
Paolo Masci   &nbs= p;      Queen Mary University of London, paol= o (dot) masci (at) eecs (dot) qmul (dot) ac (dot) uk
Dominiqu= e Mery       Universit=C3=A9 de Lorraine, dom= inique (dot) mery (at) loria (dot) fr

--------= ---------
PC MEMBERS (to be completed)
--------= ---------
Bernhard Beckert     Karlsruhe = Institute of Technology
Jose     Campos &= nbsp;    Universidade do Minho
Paul  = ;   Curzon      Queen Mary Universi= ty of London
Carlo Alberto Furia  ETH Zurich
Therese  Hardin      UPMC
Ru= stan   Leino       Microsoft Resear= ch
Michael  Leuschel    University of Dus= seldorf
Claude   Marche     &nb= sp;INRIA
Stefan   Mitsch     &n= bsp;Carnegie Mellon University
Patrick  Oladimeji  =  Swansea University
Suzette  Person   &nb= sp;  NASA Langley Research Center
Francois Pessaux =     ENSTA ParisTech
Marie-Laure Potet &nb= sp;  Laboratoire Verimag
Steve    Re= eves      Waikato University
John &n= bsp;   Rushby      SRI Internationa= l
Rene     Thiemann    Uni= versity of Innsbruck
Boris    Yakobowski  = ;CEA LIST

= --Apple-Mail=_CD9C4CF8-0B76-4B60-8E4A-07676A5C6684--