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 458297FADB for ; Mon, 3 Nov 2014 19:31:23 +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: PermError (mail3-smtp-sop.national.inria.fr: cannot correctly interpret sender authenticity information from domain of fm-announcements-bounces@lists.nasa.gov) 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 Received-SPF: PermError (mail3-smtp-sop.national.inria.fr: cannot correctly interpret sender authenticity information from domain of postmaster@lists.nasa.gov) 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-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArYBAMTIV1SAnPnlnGdsb2JhbABcFoIygRpYAcwYgWcBCYdNgScWAQEBAQERAQEBAQEICwkJFC6EBAYBARopCAIWCAYIAwECBgIaKAIECAMBJAk/BRQCAgSIIAQJyCQBAQEBHY1BAYJsCgQDAUyCQQ9EJIEeBYUbhWKIKIJfZYQSg2GBE4VvGIdviHqBa2sBgQUCBxcGgR8BAQE X-IPAS-Result: ArYBAMTIV1SAnPnlnGdsb2JhbABcFoIygRpYAcwYgWcBCYdNgScWAQEBAQERAQEBAQEICwkJFC6EBAYBARopCAIWCAYIAwECBgIaKAIECAMBJAk/BRQCAgSIIAQJyCQBAQEBHY1BAYJsCgQDAUyCQQ9EJIEeBYUbhWKIKIJfZYQSg2GBE4VvGIdviHqBa2sBgQUCBxcGgR8BAQE X-IronPort-AV: E=Sophos;i="5.07,308,1413237600"; d="scan'208,217";a="86045666" Received: from lists.nasa.gov ([128.156.249.229]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 03 Nov 2014 19:31:20 +0100 Received: from localhost (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id 184736023B0; Mon, 3 Nov 2014 13:29:55 -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 wVXOVzjY98Dh; Mon, 3 Nov 2014 13:29:54 -0500 (EST) Received: from lists.nasa.gov (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id 170A9602354; Mon, 3 Nov 2014 13:29:52 -0500 (EST) Received: from localhost (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id C4CFD60156C for ; Mon, 3 Nov 2014 13:29:48 -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 ljX-skCIbf+n for ; Mon, 3 Nov 2014 13:29:48 -0500 (EST) Received: from mail.jpl.nasa.gov (mailhost.jpl.nasa.gov [128.149.139.106]) by lists.nasa.gov (Postfix) with ESMTPS id 6102E60144D for ; Mon, 3 Nov 2014 13:29:44 -0500 (EST) Received: from [192.168.178.65] (ip-83-99-115-229.dyn.luxdsl.pt.lu [83.99.115.229]) (authenticated (0 bits)) by smtp.jpl.nasa.gov (Sentrion-MTA-4.3.1/Sentrion-MTA-4.3.1) with ESMTP id sA3ITdrR000656 (using TLSv1/SSLv3 with cipher AES128-SHA (128 bits) verified NO) for ; Mon, 3 Nov 2014 10:29:42 -0800 From: Klaus Havelund Message-Id: Date: Mon, 3 Nov 2014 19:29:44 +0100 To: fm-announcements@lists.nasa.gov Mime-Version: 1.0 (Mac OS X Mail 7.3 \(1878.6\)) X-Mailer: Apple Mail (2.1878.6) X-Source-Sender: klaus.havelund@jpl.nasa.gov X-JPL-Spam-Score': 80% 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-Type: multipart/mixed; boundary="===============8346820625180819216==" Errors-To: fm-announcements-bounces@lists.nasa.gov Sender: fm-announcements-bounces@lists.nasa.gov X-Validation-by: klaus.havelund@jpl.nasa.gov Subject: [Caml-list] [fm-announcements] NFM 2015 - deadline extension: Nov 18 --===============8346820625180819216== Content-Type: multipart/alternative; boundary="Apple-Mail=_021013A9-8C54-420F-9E8E-5294569C86D1" --Apple-Mail=_021013A9-8C54-420F-9E8E-5294569C86D1 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=windows-1252 CALL FOR PAPERS *** Deadline extension: Nov 18, 2014 *** The 7th NASA Formal Methods Symposium http://www.NASAFormalMethods.org/nfm2015 27 =96 29 April 2015 Pasadena, California, USA THEME The widespread use and increasing complexity of mission- and safety-critica= l systems require advanced techniques that address their specification, ver= ification, validation, and certification. The NASA Formal Methods Symposium is a forum for theoreticians and practiti= oners from academia, industry, and government, with the goals of identifyin= g challenges and providing solutions to achieving assurance in mission- and= safety-critical systems. Within NASA such systems include for example auto= nomous robots, separation assurance algorithms for aircraft, Next Generatio= n Air Transportation (NextGen), and autonomous rendezvous and docking for s= pacecraft. Moreover, emerging paradigms such as property-based design, code= generation, and safety cases are bringing with them new challenges and opp= ortunities. The focus of the symposium will be on formal techniques, their = theory, current capabilities, and limitations, as well as their application= to aerospace, robotics, and other mission- and safety-critical systems in = all design life-cycle stages. We encourage submissions on cross-cutting app= roaches marrying formal verification techniques with advances in critical s= ystem development, such as requirements generation, analysis of aerospace o= perational concepts, and formal methods integrated in early design stages a= nd carrying throughout system development. TOPICS Topics of interest include, but are not limited to: Model checking Theorem proving SAT and SMT solving Symbolic execution Static analysis Runtime verification Program refinement Compositional verification Modeling and specification formalisms Model-based development Model-based testing Requirement engineering Formal approaches to fault tolerance Security and intrusion detection Applications of formal methods to aerospace systems Applications of formal methods to cyber-physical systems Applications of formal methods to human-machine interaction analysis INVITED SPEAKERS Dino Distefano Software Engineer at Facebook, California, USA and Professor at Queen Mary = University of London, UK. Viktor Kuncak Leads Lab for Automated Reasoning and Analysis at EPFL, Lausanne, Switzerla= nd. Rob Manning Chief Engineer at NASA/JPL. IMPORTANT DATES Paper Submission (*** deadline extended one week ***): 18 Nov 2014 Paper Notifications: 12 Jan 2015 Camera-ready Papers: 9 Feb 2015 Symposium: 27 =96 29 April 2015 LOCATION AND COST The symposium will take place at the Hilton Hotel, Pasadena, California, US= A, April 27-29, 2015. There will be no registration fee for participants. All interested individu= als, including non-US citizens, are welcome to submit, to attend, to listen= to the talks, and to participate in discussions; however, all attendees mu= st register. SUBMISSION DETAILS There are two categories of submissions: Regular papers describing fully developed work and complete results (15 pag= es) Short papers describing tools, experience reports, or descriptions of work = in progress with preliminary results (6 pages) All papers should be in English and describe original work that has not bee= n published or submitted elsewhere. All submissions will be fully reviewed = by members of the Programme Committee. Papers will appear in a volume of Sp= ringer=92s Lecture Notes on Computer Science (LNCS), and must use LNCS styl= e formatting. Papers should be submitted in PDF format. PC CHAIRS Klaus Havelund, NASA Jet Propulsion Laboratory, USA Gerard Holzmann, NASA Jet Propulsion Laboratory, USA Rajeev Joshi, NASA Jet Propulsion Laboratory, USA PUBLICITY SUPPORT Ylies Falcone, Universit=E9 Joseph Fourier, France PROGRAMME COMMITTEE Erika Abraham, RWTH Aachen University, Germany Julia Badger, NASA Johnson Space Center, USA Christel Baier, Technische Universit=E4t Dresden, Germany Saddek Bensalem, VERIMAG/UJF, France Dirk Beyer, University of Passau, Germany Armin Biere, Johannes Kepler University, Austria Nikolaj Bjorner, Microsoft Research, USA Borzoo Bonakdarpour, McMaster University, Canada Alessandro Cimatti, Fondazione Bruno Kessler, Italy Leonardo de Moura, Microsoft Research, USA Ewen Denney, NASA Ames Research Center, USA Ben Di Vito, NASA Langley Research Center, USA Dawson Engler, Stanford University, USA Jean-Christophe Filliatre, Universit=E9 Paris-Sud, France Dimitra Giannakopoulou, NASA Ames Research Center, USA Alwyn Goodloe, NASA Langley Research Center, USA Susanne Graf, VERIMAG, France Alex Groce, Oregon State University, USA Radu Grosu, Vienna University of Technology, Austria John Harrison, Intel Corporation, USA Mike Hinchey, University of Limerick/Lero, Ireland Bart Jacobs, University of Leuven, Belgium Sarfraz Khurshid, The University of Texas at Austin, USA Gerwin Klein, NICTA, Australia Daniel Kroening, Oxford University, UK Orna Kupferman, Hebrew University Jerusalem, Israel Kim Larsen, Aalborg University, Denmark Rustan Leino, Microsoft Research, USA Martin Leucker, University of Lubeck, Germany Rupak Majumdar, Max Planck Institute, Germany Pete Manolios, Northeastern University, USA Peter Mueller, ETH Zurich, Switzerland Kedar Namjoshi, Bell Labs/Alcatel-Lucent, USA Corina Pasareanu, NASA Ames Research Center, USA Doron Peled, Bar Ilan University, Israel Suzette Person, NASA Langley Research Center, USA Andreas Podelski, University of Freiburg, Germany Grigore Rosu, University of Illinois, USA Kristin Yvonne Rozier, NASA Ames Research Center, USA Natarajan Shankar, SRI International, USA Natasha Sharygina, University of Lugano, Switzerland Scott Smolka, Stony Brook University, USA Willem Visser, University of Stellenbosch, South Africa Mahesh Viswanathan, University of Illinois, USA Mike Whalen, University of Minnesota, USA Jim Woodcock, University of York, UK STEERING COMMITTEE Julia Badger, NASA Johnson Space Center Ewen Denney, NASA Ames Research Center Ben Di Vito, NASA Langley Research Center Klaus Havelund, NASA Jet Propulsion Laboratory Gerard Holzmann, NASA Jet Propulsion Laboratory Cesar Munoz, NASA Langley Research Center Corina Pasareanu, NASA Ames Research Center Suzette Person, NASA Langley Research Center Kristin Yvonne Rozier, NASA Ames Research Center= --Apple-Mail=_021013A9-8C54-420F-9E8E-5294569C86D1 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=windows-1252

CALL FOR PAPERS

*** De= adline extension: Nov 18, 2014 ***

The 7th NASA Formal Methods Symposium

       http://www.NASAFormalMethods.=
org/nfm2015

27 =96 29 April 2015
Pa= sadena, California, USA

THEME

The widespre= ad use and increasing complexity of mission- and safety-critical systems re= quire advanced techniques that address their specification, verification, v= alidation, and certification.

The NASA Formal Methods Symposium is a forum for theoreticians and practit= ioners from academia, industry, and government, with the goals of identifyi= ng challenges and providing solutions to achieving assurance in mission- an= d safety-critical systems. Within NASA such systems include for example aut= onomous robots, separation assurance algorithms for aircraft, Next Generati= on Air Transportation (NextGen), and autonomous rendezvous and docking for = spacecraft. Moreover, emerging paradigms such as property-based design, cod= e generation, and safety cases are bringing with them new challenges and op= portunities. The focus of the symposium will be on formal techniques, their= theory, current capabilities, and limitations, as well as their applicatio= n to aerospace, robotics, and other mission- and safety-critical systems in= all design life-cycle stages. We encourage submissions on cross-cutting ap= proaches marrying formal verification techniques with advances in critical = system development, such as requirements generation, analysis of aerospace = operational concepts, and formal methods integrated in early design stages = and carrying throughout system development.

TOPICS

Topics of interest include, but are not limited to:

  • Model checking
  • Theorem proving
  • SAT and SMT solving
  • Symbolic execution
  • Static analysis
  • Runtime verification
    • =
  • Program refin= ement
  • Com= positional verification
  • Modeling and specification formalisms
  • Model-based development
    • Model-based test= ing
  • Requi= rement engineering
  • Formal approaches to fault tolerance
  • Security and intrusion detection
    • =
  • Applications = of formal methods to aerospace systems
  • Applications of formal methods to cyber-physi= cal systems
  • Applications of formal methods to human-machine interaction analysis

INVITED SPE= AKERS

Dino Distefano
Software Engineer at= Facebook, California, USA and Professor at Queen Mary University of London= , UK.

Viktor Kuncak
Leads Lab for Automated Reas= oning and Analysis at EPFL, Lausanne, Switzerland.

Rob Manning
Chief Engineer at NASA/JPL.

IMPORTANT DATES

Paper Submission= (*** deadline extended one week ***):18 Nov 2014= Paper Notifications:12 Jan= 2015Camera-= ready Papers:9 Feb 2015Symposium:27 =96 29 April 2015

LOCATION AND COST

The symposium will take place at the Hilton= Hotel, Pasadena, California, USA, April 27-29, 2015.

There will be no registration fee for participants= . All interested individuals, including non-US citizens, are welcome to sub= mit, to attend, to listen to the talks, and to participate in discussions; = however, all attendees must register.

SUBMISSION DETAILS

There are two categories of submissions:

  1. Sho= rt papers describing tools, experience reports, or descriptions of work in = progress with preliminary results (6 pages)

All papers should be in English and describe original = work that has not been published or submitted elsewhere. All submissions wi= ll be fully reviewed by members of the Programme Committee. Papers will app= ear in a volume of Springer=92s Lecture Notes on Computer Science (LNCS), a= nd must use LNCS style formatting. Papers should be submitted in PDF format= .

PC CHAIRS

Klaus Havelund, NASA Jet Propu= lsion Laboratory, USA
Gerard Holzmann, NASA Jet Propulsion Laboratory, U= SA
Rajeev Joshi, NASA Jet Propulsion Laboratory, USA

PUBLICITY SUPPORT

Ylies Falcone, Universit=E9 Joseph Fourier,= France

PROGRA= MME COMMITTEE

Erika Abraham,= RWTH Aachen University, Germany
Julia Badger, NASA Johnson Space Center= , USA
Christel Baier, Technische Universit=E4t Dresden, Germany
Sadde= k Bensalem, VERIMAG/UJF, France
Dirk Beyer, University of Passau, German= y
Armin Biere, Johannes Kepler University, Austria
Nikolaj Bjorner, M= icrosoft Research, USA
Borzoo Bonakdarpour, McMaster University, Canada<= br>Alessandro Cimatti, Fondazione Bruno Kessler, Italy
Leonardo de Moura= , Microsoft Research, USA
Ewen Denney, NASA Ames Research Center, USABen Di Vito, NASA Langley Research Center, USA
Dawson Engler, Stanford = University, USA
Jean-Christophe Filliatre, Universit=E9 Paris-Sud, Franc= e
Dimitra Giannakopoulou, NASA Ames Research Center, USA
Alwyn Goodlo= e, NASA Langley Research Center, USA
Susanne Graf, VERIMAG, France
Al= ex Groce, Oregon State University, USA
Radu Grosu, Vienna University of = Technology, Austria
John Harrison, Intel Corporation, USA
Mike Hinche= y, University of Limerick/Lero, Ireland
Bart Jacobs, University of Leuve= n, Belgium
Sarfraz Khurshid, The University of Texas at Austin, USA
G= erwin Klein, NICTA, Australia
Daniel Kroening, Oxford University, UK
= Orna Kupferman, Hebrew University Jerusalem, Israel
Kim Larsen, Aalborg = University, Denmark
Rustan Leino, Microsoft Research, USA
Martin Leuc= ker, University of Lubeck, Germany
Rupak Majumdar, Max Planck Institute,= Germany
Pete Manolios, Northeastern University, USA
Peter Mueller, E= TH Zurich, Switzerland
Kedar Namjoshi, Bell Labs/Alcatel-Lucent, USA
= Corina Pasareanu, NASA Ames Research Center, USA
Doron Peled, Bar Ilan U= niversity, Israel
Suzette Person, NASA Langley Research Center, USA
A= ndreas Podelski, University of Freiburg, Germany
Grigore Rosu, Universit= y of Illinois, USA
Kristin Yvonne Rozier, NAS= A Ames Research Center, USA
Natarajan Shankar, SRI International, USANatasha Sharygina, University of Lugano, Switzerland
Scott Smolka, Ston= y Brook University, USA
Willem Visser, University of Stellenbosch, South= Africa
Mahesh Viswanathan, University of Illinois, USA
Mike Whalen, = University of Minnesota, USA
Jim Woodcock, University of York, UK

STEERING COMMITTEE

Julia Badger, NASA Johnson Sp= ace Center
Ewen Denney, NASA Ames Research Center
Ben Di Vito, NASA L= angley Research Center
Klaus Havelund, NASA Jet Propulsion LaboratoryGerard Holzmann, NASA Jet Propulsion Laboratory
Cesar Munoz, NASA Langl= ey Research Center
Corina Pasareanu, NASA Ames Research Center
Suzett= e Person, NASA Langley Research Center
Kristin Yvonne Rozier, NASA Ames Research Center

= --Apple-Mail=_021013A9-8C54-420F-9E8E-5294569C86D1-- --===============8346820625180819216== Content-Type: text/plain; charset="us-ascii" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Disposition: inline --- 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 the request by contacting fm-announcements-owner@lists.nasa.gov --===============8346820625180819216==--