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 50CE37FADB for ; Mon, 3 Nov 2014 19:44:19 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of compscience.announcement@gmail.com) identity=pra; client-ip=209.85.217.194; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="compscience.announcement@gmail.com"; x-sender="compscience.announcement@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of compscience.announcement@gmail.com designates 209.85.217.194 as permitted sender) identity=mailfrom; client-ip=209.85.217.194; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="compscience.announcement@gmail.com"; x-sender="compscience.announcement@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-lb0-f194.google.com) identity=helo; client-ip=209.85.217.194; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="compscience.announcement@gmail.com"; x-sender="postmaster@mail-lb0-f194.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: As0DAEnMV1TRVdnClGdsb2JhbABcFoIygRpNCwSDArc5kVqBZwEJh02BIAcWAQEBAQERAQEBAQcLCwkSMIQbCwYdARsKDgYDEhAFKAoCJAERAQUBIhsRAgeICQEDEg2kSoMhPTGLM4FygxGILAoZJw1ohSkBCwEZAQUOhimHCoJ3BFCCQQ8yEoFCBYUbhWKIKIJfZYcYW4ETjXaEcRgpg0iBazwvAYEFAh4GgR8BAQE X-IPAS-Result: As0DAEnMV1TRVdnClGdsb2JhbABcFoIygRpNCwSDArc5kVqBZwEJh02BIAcWAQEBAQERAQEBAQcLCwkSMIQbCwYdARsKDgYDEhAFKAoCJAERAQUBIhsRAgeICQEDEg2kSoMhPTGLM4FygxGILAoZJw1ohSkBCwEZAQUOhimHCoJ3BFCCQQ8yEoFCBYUbhWKIKIJfZYcYW4ETjXaEcRgpg0iBazwvAYEFAh4GgR8BAQE X-IronPort-AV: E=Sophos;i="5.07,308,1413237600"; d="scan'208";a="86047973" Received: from mail-lb0-f194.google.com ([209.85.217.194]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 03 Nov 2014 19:44:18 +0100 Received: by mail-lb0-f194.google.com with SMTP id w7so584712lbi.1 for ; Mon, 03 Nov 2014 10:44:17 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:date:message-id:subject:from:to:content-type; bh=kqDdCfhbbEsTQQdcd6ePWuj6tfzgR1qsUbBZXBCLgkM=; b=qtDswh1a/NmKQm0tBlVczwHtWFWZtt2VAwCugbvuhpPdzzxBzjgIHJvHOda8jmfKoD PBleEzrLrd6QKBYTTWBTOmrc2ykmQuPvyMJsUD2pG+HpAdd5XWgH2CM/1Zxh5JGHcVUT HskB/vvbktgkvSMeJ4uhB4AL+yyIqWIYNEI4rUUZbTTUj5bDYwHehBrah98FlawbvyRe nDFVHXuCtgc7yYy5zRA4EX4ys4jq26eRfMjboyFkmLmwcKRxRU9aEXyQy8H4r1Kr3Z8Z VMbdvgzwiJIDtgDky/fZZsT+n2JSPvdVuSCt+FBolsdCAn9xKQ2uW4OcEmSUuwBMzXaY hxRA== MIME-Version: 1.0 X-Received: by 10.112.48.3 with SMTP id h3mr53717735lbn.71.1415039856589; Mon, 03 Nov 2014 10:37:36 -0800 (PST) Received: by 10.152.20.194 with HTTP; Mon, 3 Nov 2014 10:37:36 -0800 (PST) Date: Mon, 3 Nov 2014 19:37:36 +0100 Message-ID: From: Klaus Havelund To: Klaus Havelund Content-Type: multipart/alternative; boundary=001a11348304fec88d0506f8a31a Subject: [Caml-list] NFM 2015 - deadline extension: Nov 18 --001a11348304fec88d0506f8a31a Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable CALL FOR PAPERS *** Deadline extension: Nov 18, 2014 *** The 7th NASA Formal Methods Symposium http://www.NASAFormalMethods.org/nfm2015 27 =E2=80=93 29 April 2015 Pasadena, California, USA THEME The widespread use and increasing complexity of mission- and safety-critical systems require advanced techniques that address their specification, verification, validation, and certification. The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, industry, and government, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. Within NASA such systems include for example autonomous robots, separation assurance algorithms for aircraft, Next Generation Air Transportation (NextGen), and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms such as property-based design, code generation, and safety cases are bringing with them new challenges and opportunities. 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 approaches 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 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, Switzerland. Rob Manning Chief Engineer at NASA/JPL. IMPORTANT DATESPaper Submission (*** deadline extended one week ***):18 Nov 2014Paper Notifications:12 Jan 2015Camera-ready Papers:9 Feb 2015Symposium:= 27 =E2=80=93 29 April 2015LOCATION 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 submit, 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. Regular papers describing fully developed work and complete results (15 pages) 2. 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 been published or submitted elsewhere. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in a volume of Springer=E2=80=99s Lecture Notes on Computer Science (LNCS), and = must use LNCS style 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=C3=A9 Joseph Fourier, France PROGRAMME COMMITTEE Erika Abraham, RWTH Aachen University, Germany Julia Badger, NASA Johnson Space Center, USA Christel Baier, Technische Universit=C3=A4t 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=C3=A9 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 --001a11348304fec88d0506f8a31a Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

CALL FOR PAPERS

*** Deadline= extension: Nov 18, 2014 ***

The 7th NASA Form= al Methods Symposium

       htt=
p://www.NASAFormalMethods.org/nfm2015

27 =E2=80=93 29 April 2015
Pasadena, Califor= nia, USA

THEME

The widespread use and increasing complexity of mission- and safety-cri= tical systems require advanced techniques that address their specification,= verification, validation, and certification.

The = NASA Formal Methods Symposium is a forum for theoreticians and practitioner= s from academia, industry, and government, with the goals of identifying ch= allenges and providing solutions to achieving assurance in mission- and saf= ety-critical systems. Within NASA such systems include for example autonomo= us robots, separation assurance algorithms for aircraft, Next Generation Ai= r Transportation (NextGen), and autonomous rendezvous and docking for space= craft. Moreover, emerging paradigms such as property-based design, code gen= eration, and safety cases are bringing with them new challenges and opportu= nities. The focus of the symposium will be on formal techniques, their theo= ry, 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 approac= hes marrying formal verification techniques with advances in critical syste= m development, such as requirements generation, analysis of aerospace opera= tional concepts, and formal methods integrated in early design stages and c= arrying 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 m= ethods to aerospace systems
  • Applications of formal methods to cyber-physical systems
  • Applications of formal methods to hu= man-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 Auto= mated Reasoning and Analysis at EPFL, Lausanne, Switzerland.

Rob Mannin= g
Chief Engineer at NASA/JPL.

= IMPORTANT DATES

LOCATION AND COST

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

There will be no regi= stration fee for participants. All interested individuals, including non-US= citizens, are welcome to submit, 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. Re= gular papers describing fully developed work and complete results (15 pages= )
  2. Short papers describi= ng tools, experience reports, or descriptions of work in progress with prel= iminary results (6 pages)

All papers should = be in English and describe original work that has not been published or sub= mitted elsewhere. All submissions will be fully reviewed by members of the = Programme Committee. Papers will appear in a volume of Springer=E2=80=99s L= ecture Notes on Computer Science (LNCS), and must use LNCS style formatting= . Papers should be submitted in PDF format.

PC CHAIRS

Klaus Havelund, NASA Jet Propuls= ion Laboratory, USA
Gerard Holzmann, NASA Jet Propulsion Laboratory, USA=
Rajeev Joshi, NASA Jet Propulsion Laboratory, USA

PUBLICITY SUPPORT

Ylies Falcone,= Universit=C3=A9 Joseph Fourier, France

PROGRAMME COMMITTEE

Erika Abraham, RWTH Aachen= University, Germany
Julia Badger, NASA Johnson Space Center, USA
Chr= istel Baier, Technische Universit=C3=A4t Dresden, Germany
Saddek Bensale= m, VERIMAG/UJF, France
Dirk Beyer, University of Passau, Germany
Armi= n Biere, Johannes Kepler University, Austria
Nikolaj Bjorner, Microsoft = Research, USA
Borzoo Bonakdarpour, McMaster University, Canada
Alessa= ndro Cimatti, Fondazione Bruno Kessler, Italy
Leonardo de Moura, Microso= ft Research, USA
Ewen Denney, NASA Ames Research Center, USA
Ben Di V= ito, NASA Langley Research Center, USA
Dawson Engler, Stanford Universit= y, USA
Jean-Christophe Filliatre, Universit=C3=A9 Paris-Sud, France
D= imitra Giannakopoulou, NASA Ames Research Center, USA
Alwyn Goodloe, NAS= A Langley Research Center, USA
Susanne Graf, VERIMAG, France
Alex Gro= ce, Oregon State University, USA
Radu Grosu, Vienna University of Techno= logy, Austria
John Harrison, Intel Corporation, USA
Mike Hinchey, Uni= versity of Limerick/Lero, Ireland
Bart Jacobs, University of Leuven, Bel= gium
Sarfraz Khurshid, The University of Texas at Austin, USA
Gerwin = Klein, NICTA, Australia
Daniel Kroening, Oxford University, UK
Orna K= upferman, Hebrew University Jerusalem, Israel
Kim Larsen, Aalborg Univer= sity, Denmark
Rustan Leino, Microsoft Research, USA
Martin Leucker, U= niversity of Lubeck, Germany
Rupak Majumdar, Max Planck Institute, Germa= ny
Pete Manolios, Northeastern University, USA
Peter Mueller, ETH Zur= ich, Switzerland
Kedar Namjoshi, Bell Labs/Alcatel-Lucent, USA
Corina= Pasareanu, NASA Ames Research Center, USA
Doron Peled, Bar Ilan Univers= ity, Israel
Suzette Person, NASA Langley Research Center, USA
Andreas= Podelski, University of Freiburg, Germany
Grigore Rosu, University of I= llinois, USA
Kristin=C2=A0Yvonne=C2=A0Rozier, NASA Ames Research Center, = USA
Natarajan Shankar, SRI International, USA
Natasha Sharygina, Univ= ersity of Lugano, Switzerland
Scott Smolka, Stony Brook University, USA<= br>Willem Visser, University of Stellenbosch, South Africa
Mahesh Viswan= athan, University of Illinois, USA
Mike Whalen, University of Minnesota,= USA
Jim Woodcock, University of York, UK

STEERING COMMITTEE

Julia Badger, NASA Joh= nson Space Center
Ewen Denney, NASA Ames Research Center
Ben Di Vito,= NASA Langley Research Center
Klaus Havelund, NASA Jet Propulsion Labora= tory
Gerard Holzmann, NASA Jet Propulsion Laboratory
Cesar Munoz, NAS= A Langley Research Center
Corina Pasareanu, NASA Ames Research CenterSuzette Person, NASA Langley Research Center
Kristin=C2=A0Yvonne=C2=A0= Rozier, NASA Ames Research Center

--001a11348304fec88d0506f8a31a--
Paper Subm= ission (***= deadline extended one week ***):18 Nov = 2014
Paper Notifications:12 Jan 2015
Camera-ready Papers:9 Feb 2015
Symposium:27 =E2=80=93 29 April 2015