CALL FOR PAPERSThe 7th NASA Formal Methods Symposiumhttp://www.NASAFormalMethods.org/nfm201527 – 29 April 2015Pasadena, California, USAPaper Submission: *** 10 Nov 2014 ***THEMEThe 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.TOPICSTopics of interest include, but are not limited to:Model checkingTheorem provingSAT and SMT solvingSymbolic executionStatic analysisRuntime verificationProgram refinementCompositional verificationModeling and specification formalismsModel-based developmentModel-based testingRequirement engineeringFormal approaches to fault toleranceSecurity and intrusion detectionApplications of formal methods to aerospace systemsApplications of formal methods to cyber-physical systemsApplications of formal methods to human-machine interaction analysisINVITED SPEAKERSDino DistefanoSoftware Engineer at Facebook, California, USA and Professor at Queen Mary University of London, UK.Viktor KuncakLeads Lab for Automated Reasoning and Analysis at EPFL, Lausanne, Switzerland.Rob ManningChief Engineer at NASA/JPL.IMPORTANT DATESPaper Submission: 10 Nov 2014Paper Notifications: 12 Jan 2015Camera-ready Papers: 9 Feb 2015Symposium: 27 – 29 April 2015LOCATION AND COSTThe 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 DETAILSThere are two categories of submissions:- Regular papers describing fully developed work and complete results (15 pages)- 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’s Lecture Notes on Computer Science (LNCS), and must use LNCS style formatting. Papers should be submitted in PDF format.PC CHAIRSKlaus Havelund, NASA Jet Propulsion LaboratoryGerard Holzmann, NASA Jet Propulsion LaboratoryRajeev Joshi, NASA Jet Propulsion LaboratoryPROGRAMME COMMITTEEErika Abraham, RWTH Aachen University, GermanyJulia Badger, NASA Johnson Space Center, USAChristel Baier, Technische Universität Dresden, GermanySaddek Bensalem, VERIMAG/UJF, FranceDirk Beyer, University of Passau, GermanyArmin Biere, Johannes Kepler University, AustriaNikolaj Bjorner, Microsoft Research, USABorzoo Bonakdarpour, McMaster University, CanadaAlessandro Cimatti, Fondazione Bruno Kessler, ItalyLeonardo de Moura, Microsoft Research, USAEwen Denney, NASA Ames Research Center, USABen Di Vito, NASA Langley Research Center, USADawson Engler, Stanford University, USAJean-Christophe Filliatre, Université Paris-Sud, FranceDimitra Giannakopoulou, NASA Ames Research Center, USAAlwyn Goodloe, NASA Langley Research Center, USASusanne Graf, VERIMAG, FranceAlex Groce, Oregon State University, USARadu Grosu, Vienna University of Technology, AustriaJohn Harrison, Intel Corporation, USAMike Hinchey, University of Limerick/Lero, IrelandBart Jacobs, University of Leuven, BelgiumSarfraz Khurshid, The University of Texas at Austin, USAGerwin Klein, NICTA, AustraliaDaniel Kroening, Oxford University, UKOrna Kupferman, Hebrew University Jerusalem, IsraelKim Larsen, Aalborg University, DenmarkRustan Leino, Microsoft Research, USAMartin Leucker, University of Lubeck, GermanyRupak Majumdar, Max Planck Institute, GermanyPete Manolios, Northeastern University, USAPeter Mueller, ETH Zurich, SwitzerlandKedar Namjoshi, Bell Labs/Alcatel-Lucent, USACorina Pasareanu, NASA Ames Research Center, USADoron Peled, Bar Ilan University, IsraelSuzette Person, NASA Langley Research Center, USAAndreas Podelski, University of Freiburg, GermanyGrigore Rosu, University of Illinois, USAKristin Yvonne Rozier, NASA Ames Research Center, USANatarajan Shankar, SRI International, USANatasha Sharygina, University of Lugano, SwitzerlandScott Smolka, Stony Brook University, USAWillem Visser, University of Stellenbosch, South AfricaMahesh Viswanathan, University of Illinois, USAMike Whalen, University of Minnesota, USAJim Woodcock, University of York, UKSTEERING COMMITTEEJulia Badger, NASA Johnson Space CenterEwen Denney, NASA Ames Research CenterBen Di Vito, NASA Langley Research CenterKlaus Havelund, NASA Jet Propulsion LaboratoryGerard Holzmann, NASA Jet Propulsion LaboratoryCesar Munoz, NASA Langley Research CenterCorina Pasareanu, NASA Ames Research CenterSuzette Person, NASA Langley Research CenterKristin Yvonne Rozier, NASA Ames Research Center---