From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id D243F7EE25 for ; Tue, 5 Nov 2013 17:47:34 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of fm-announcements-bounces@lists.nasa.gov) identity=pra; client-ip=128.156.249.229; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="fm-announcements-bounces@lists.nasa.gov"; x-sender="fm-announcements-bounces@lists.nasa.gov"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of fm-announcements-bounces@lists.nasa.gov designates 128.156.249.229 as permitted sender) identity=mailfrom; client-ip=128.156.249.229; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="fm-announcements-bounces@lists.nasa.gov"; x-sender="fm-announcements-bounces@lists.nasa.gov"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of postmaster@lists.nasa.gov designates 128.156.249.229 as permitted sender) identity=helo; client-ip=128.156.249.229; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="fm-announcements-bounces@lists.nasa.gov"; x-sender="postmaster@lists.nasa.gov"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsEFAOcfeVKAnPnlm2dsb2JhbABWA4M/U8BjFg4BAQEBAQYLCwkUJwGCJwYBARopCAIeBgQEAwECBQECKxYDBAgDAQUDAgECAQkNCTIBBgYCAQEBFAICBIdgDb5yBI4MCoFXgmmBNQOJCDiLfYJNlVCBRwIHFwYc X-IPAS-Result: AsEFAOcfeVKAnPnlm2dsb2JhbABWA4M/U8BjFg4BAQEBAQYLCwkUJwGCJwYBARopCAIeBgQEAwECBQECKxYDBAgDAQUDAgECAQkNCTIBBgYCAQEBFAICBIdgDb5yBI4MCoFXgmmBNQOJCDiLfYJNlVCBRwIHFwYc X-IronPort-AV: E=Sophos;i="4.93,640,1378850400"; d="scan'208";a="33868531" Received: from lists.nasa.gov ([128.156.249.229]) by mail3-smtp-sop.national.inria.fr with ESMTP; 05 Nov 2013 17:47:33 +0100 Received: from localhost (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id 74F03602427; Tue, 5 Nov 2013 11:46:00 -0500 (EST) Received: from lists.nasa.gov ([127.0.0.1]) by localhost (lists.nasa.gov [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 43Qnkj1SCPae; Tue, 5 Nov 2013 11:46:00 -0500 (EST) Received: from lists.nasa.gov (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id AC43F6022B6; Tue, 5 Nov 2013 11:45:57 -0500 (EST) Received: from localhost (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id 90652601CB3 for ; Tue, 5 Nov 2013 11:43:31 -0500 (EST) Received: from lists.nasa.gov ([127.0.0.1]) by localhost (lists.nasa.gov [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id nLr+QgTqP5Sf for ; Tue, 5 Nov 2013 11:43:31 -0500 (EST) Received: from ndjsnpf01.ndc.nasa.gov (ndjsnpf01.ndc.nasa.gov [198.117.1.121]) by lists.nasa.gov (Postfix) with ESMTP id 6AA4E6007F1 for ; Tue, 5 Nov 2013 11:43:31 -0500 (EST) Received: from ndmsppt104.ndc.nasa.gov (ndmsppt104.ndc.nasa.gov [198.117.0.69]) by ndjsnpf01.ndc.nasa.gov (Postfix) with ESMTP id A464BD0572; Tue, 5 Nov 2013 10:43:40 -0600 (CST) Received: from NDMSCHT114.ndc.nasa.gov (ndmscht114-pub.ndc.nasa.gov [198.117.0.214]) by ndmsppt104.ndc.nasa.gov (8.14.5/8.14.5) with ESMTP id rA5GhUpO012151; Tue, 5 Nov 2013 10:43:30 -0600 Received: from logique.ndc.nasa.gov (50.168.53.123) by smtp02.ndc.nasa.gov (198.117.0.214) with Microsoft SMTP Server (TLS) id 14.3.158.1; Tue, 5 Nov 2013 10:43:30 -0600 Message-ID: <5279202E.1050700@nasa.gov> Date: Tue, 5 Nov 2013 08:43:26 -0800 From: Kristin Yvonne Rozier User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.12) Gecko/20130108 Thunderbird/10.0.12 MIME-Version: 1.0 To: undisclosed-recipients:; X-Originating-IP: [50.168.53.123] X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:5.10.8794, 1.0.431, 0.0.0000 definitions=2013-11-05_06:2013-11-05,2013-11-05,1970-01-01 signatures=0 X-Mailman-Approved-At: Tue, 05 Nov 2013 11:45:55 -0500 X-BeenThere: fm-announcements@lists.nasa.gov X-Mailman-Version: 2.1.14 List-Id: NASA Formal Methods Announcements List-Unsubscribe: , List-Post: List-Help: List-Subscribe: , Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="iso-8859-1"; Format="flowed" Errors-To: fm-announcements-bounces@lists.nasa.gov Sender: fm-announcements-bounces@lists.nasa.gov X-Validation-by: kristin.y.rozier@nasa.gov Subject: [Caml-list] [fm-announcements] Last Call for Papers: NASA Formal Methods (NFM) 2014 ************************************************** The Sixth NASA Formal Methods Symposium http://www.NASAFormalMethods.org/ 29 April - 1 May 2014 NASA Johnson Space Center, Houston, Texas, USA ************************************************** Theme of the Symposium: ----------------------- The widespread use and increasing complexity of mission- and=20 safety-critical systems require advanced techniques that address their=20 specification, verification, validation, and certification requirements. The NASA Formal Methods Symposium is a forum for theoreticians and=20 practitioners from academia, industry, and government, with the goals of=20 identifying challenges and providing solutions to achieving assurance in=20 mission- and safety-critical systems. Within NASA such systems include=20 autonomous robots, separation assurance algorithms for aircraft, Next=20 Generation Air Transportation (NextGen), and autonomous rendezvous and=20 docking for spacecraft. Moreover, emerging paradigms such as=20 property-based design, code generation, and safety cases are bringing=20 with them new challenges and opportunities. The focus of the symposium=20 will be on formal techniques, their theory, current capabilities, and=20 limitations, as well as their application to aerospace, robotics, and=20 other safety-critical systems in all design life-cycle stages. We=20 encourage submissions on cross-cutting approaches marrying formal=20 verification techniques with advances in safety-critical system=20 development, such as requirements generation, analysis of aerospace=20 operational concepts, and formal methods integrated in early design=20 stages carrying throughout system development. Topics of Interest: ------------------- * Model checking * Theorem proving * Static analysis * Model-based development * Runtime monitoring * Formal approaches to fault tolerance * Applications of formal methods to aerospace systems * Formal analysis of cyber-physical systems, including hybrid and=20 embedded systems * Formal methods in systems engineering, modeling, requirements,=20 and specifications * Requirements generation, specification debugging, formal=20 validation of specifications * Use of formal methods in safety cases * Use of formal methods in human-machine interaction analysis * Formal methods for parallel hardware implementations * Use of formal methods in automated software engineering and testing * Correct-by-design, design for verification, and property-based=20 design techniques * Techniques and algorithms for scaling formal methods; e.g.=20 abstraction and symbolic methods, compositional techniques, parallel and=20 distributed techniques * Application of formal methods to emerging technologies Important Dates: ---------------- Abstract Submission: 14 Nov 2013 Paper Submission: 21 Nov 2013 Paper Notifications: 14 Jan 2014 Camera-ready Papers: 11 Feb 2014 Symposium: 29 April - 1 May 2014 Location & Cost: ---------------- The symposium will take place at the Gilruth Center, NASA Johnson Space=20 Center, Houston, Texas, USA, 29 April to 1 May 2013. There will be no registration fee for participants. All interested=20 individuals, including non-US citizens, are welcome to attend, to listen=20 to the talks, and to participate in discussions; however, all attendees=20 must register. Submission Details: ------------------- There are two categories of submissions: 1. Regular papers describing fully developed work and complete=20 results (15 pages) 2. Short papers describing tools, experience reports, or=20 descriptions of work in progress with preliminary results (6 pages) All papers should be in English and describe original work that has not=20 been published or submitted elsewhere. All submissions will be fully=20 reviewed by members of the Programme Committee. Papers will appear in a=20 volume of Springer's Lecture Notes on Computer Science (LNCS), and must=20 use LNCS style formatting. Papers should be submitted in PDF format. Keynote Speakers: ----------------- * Larry Paulson, University of Cambridge, UK * Moshe Y. Vardi, Rice University, USA * Special Guest Talk: "NASA Future Challenges in Formal Methods" by Bill McAllister, Chief, Safety and Mission Assurance, International=20 Space Station Safety Panels, Avionics and Software Branch Panel Feature: "Future Directions of Specifications for Formal Methods" ----------------------------------------------------------------------- Panelists: Matt Dwyer, University of Nebraska, USA Hadas Kress-Gazit, Cornell University, USA Moshe Y. Vardi, Rice University, USA Panel Description: Specifications are required for all applications of=20 formal methods yet extracting specifications for real-life safety=20 critical systems often proves to be a huge bottleneck or even an=20 insurmountable hurdle to the application of formal methods in practice.=20 This is the state for safety-critical systems today and as these systems=20 grow more complex, more pervasive, and more powerful in the future,=20 there is not a clear path even for maintaining the bleak status quo.=20 Therefore, we propose highlighting this issue in the home of an=20 important critical system, the Mission Control Center of NASA's most=20 famous critical systems, and asking our panelists where we can go from here. Organizers: ----------- Mike Hinchey (General Chair) Julia Badger (PC Chair) Kristin Yvonne Rozier (PC Chair) Program Committee: ------------------ Domagoj Babic, Google Research, USA Calin Belta, Boston University, USA Armin Biere, Johannes Kepler University, Austria Nikolaj Bjorner, Microsoft Research, USA Jonathan P. Bowen, Museophile Limited, UK Guillaume Brat, CMU/NASA Ames Research Center, USA Gianfranco Ciardo, Iowa State University, USA Frederic Dadeau, FEMTO-ST/INRIA, France Ewen Denney, SGT/NASA Ames Research Center, USA Ben Di Vito, NASA Langley Research Center, USA James Disbrow, NASA Dryden Flight Research Center, USA Steven Drager, Air Force Research Laboratory, USA Alexandre Duret-Lutz, LRDE/EPITA, France Cindy Eisner, IBM Research-Haifa, Israel =C9ric F=E9ron, Georgia Institute of Technology, USA Shalini Ghosh, SRI, USA Alwyn Goodloe, NASA Langley Research Center, USA Arie Gurfinkel, Carnegie Mellon University Software Engineering=20 Institute, USA John Harrison, Intel Corporation, USA Klaus Havelund, NASA/Jet Propulsion Laboratory, USA Connie Heitmeyer, Naval Research Laboratory, USA Gerard Holzmann, NASA/Jet Propulsion Laboratory, USA Hadas Kress-Gazit, Cornell University, USA Joe Leslie-Hurd, Intel Corporation, USA David R. Lester, University of Manchester, UK Kenneth McMillan, Microsoft Research, USA Steven Miller, Rockwell Collins, USA Sheena Judson Miller, Barrios Technology/NASA Johnson Space Center, USA Cesar Munoz, NASA Langley Research Center, USA Suzette Person, NASA Langley Research Center, USA Lee Pike, Galois, Inc., USA Andr=E9 Platzer, Carnegie Mellon University, USA Neha Rungta, NASA Ames Research Center, USA Johann Schumann, SGT/NASA Ames Research Center, USA Cristina Seceleanu, M=E4lardalen University, Sweden Sandeep K. Shukla, Virginia Tech, USA Radu Siminiceanu Oksana Tkachuk, NASA Ames Research Center, USA Stefano Tonetta, FBK-irst, Italy Helmut Veith, Vienna University of Technology, Austria Arnaud Venet, CMU/NASA Ames Research Center, USA Mike Whalen, University of Minnesota Software Engineering Center, USA Nok Wongpiromsarn, Singapore-MIT Alliance for Research and Technology,=20 Singapore Karen Yorav, IBM Haifa Research Lab, Israel Steering Committee: ------------------- Ewen Denney, SGT/NASA Ames Ben Di Vito, NASA Langley Klaus Havelund, NASA/JPL Gerard Holzmann, NASA/JPL Cesar Munoz, NASA Langley Corina Pasareanu, CMU/NASA Ames Suzette Person, NASA Langley Kristin Y. Rozier, NASA Ames --=20 ____________________________________________________________ __ /\ \ \_____ / \ ###[=3D=3D_____> / \ /_/ __ / __ \ \ \_____ | ( ) | ###[=3D=3D_____> /| /\/\ |\ /_/ / | | | | \ / |=3D|=3D=3D|=3D| \ Kristin Yvonne Rozier, Ph.D. / | | | | \ Research Computer Scientist / USA | ~||~ |NASA \ NASA Ames Research Center |______| ~~ |______| Phone: (650) 604-3197 (__||__) Fax: (650) 604-3594 /_\ /_\ !!! !!! http://ti.arc.nasa.gov/profile/kyrozier/ Any opinions expressed in this email are my own. --- To opt-out from this mailing list, send an email to fm-announcements-request@lists.nasa.gov with the word 'unsubscribe' as subject or in the body. You can also make th= e request by contacting fm-announcements-owner@lists.nasa.gov=20