<div dir="ltr"><h3 style="border:0px;font-family:Lato,sans-serif;font-size:22px;margin:0px 0px 12px;outline:0px;padding:0px;vertical-align:baseline;clear:both;line-height:24px;color:rgb(43,43,43)">CALL FOR PAPERS</h3><div style="color:rgb(0,0,0);font-family:Courier;font-size:18px">*** Deadline extension: Nov 18, 2014 ***</div><div style="color:rgb(0,0,0);font-family:Courier;font-size:18px"><br></div><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px">The 7th NASA Formal Methods Symposium</p><pre style="border:1px solid rgba(0,0,0,0.0980392);font-family:monospace,serif;font-size:15px;margin-top:0px;margin-bottom:24px;outline:0px;padding:12px;vertical-align:baseline;line-height:24px;max-width:100%;overflow:auto;white-space:pre-wrap;word-wrap:break-word;color:rgb(43,43,43)">       <a href="http://www.nasaformalmethods.org/nfm2015">http://www.NASAFormalMethods.org/nfm2015</a>
</pre><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px">27 – 29 April 2015<br>Pasadena, California, USA</p><h4 style="border:0px;font-family:Lato,sans-serif;font-size:20px;margin:36px 0px 12px;outline:0px;padding:0px;vertical-align:baseline;clear:both;line-height:24px;color:rgb(43,43,43)">THEME</h4><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px">The widespread use and increasing complexity of mission- and safety-critical systems require advanced techniques that address their specification, verification, validation, and certification.</p><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px">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.</p><h4 style="border:0px;font-family:Lato,sans-serif;font-size:20px;margin:36px 0px 12px;outline:0px;padding:0px;vertical-align:baseline;clear:both;line-height:24px;color:rgb(43,43,43)">TOPICS</h4><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px">Topics of interest include, but are not limited to:</p><ul style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px 20px;outline:0px;padding:0px;vertical-align:baseline;list-style-position:initial;color:rgb(43,43,43);line-height:24px"><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Model checking</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Theorem proving</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">SAT and SMT solving</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Symbolic execution</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Static analysis</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Runtime verification</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Program refinement</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Compositional verification</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Modeling and specification formalisms</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Model-based development</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Model-based testing</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Requirement engineering</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Formal approaches to fault tolerance</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Security and intrusion detection</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Applications of formal methods to aerospace systems</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Applications of formal methods to cyber-physical systems</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Applications of formal methods to human-machine interaction analysis</li></ul><h4 style="border:0px;font-family:Lato,sans-serif;font-size:20px;margin:36px 0px 12px;outline:0px;padding:0px;vertical-align:baseline;clear:both;line-height:24px;color:rgb(43,43,43)">INVITED SPEAKERS</h4><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px"><a href="http://www.eecs.qmul.ac.uk/~ddino/" style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(36,137,13)">Dino Distefano</a><br>Software Engineer at Facebook, California, USA and Professor at Queen Mary University of London, UK.</p><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px"><a href="http://lara.epfl.ch/~kuncak/" style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(36,137,13)">Viktor Kuncak</a><br>Leads Lab for Automated Reasoning and Analysis at EPFL, Lausanne, Switzerland.</p><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px"><a href="https://www.linkedin.com/pub/rob-manning/54/16a/71b" style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(36,137,13)">Rob Manning</a><br>Chief Engineer at NASA/JPL.</p><h4 style="border:0px;font-family:Lato,sans-serif;font-size:20px;margin:36px 0px 12px;outline:0px;padding:0px;vertical-align:baseline;clear:both;line-height:24px;color:rgb(43,43,43)">IMPORTANT DATES</h4><table style="border-width:1px 0px 0px 1px;border-style:solid;border-color:rgba(0,0,0,0.0980392);font-family:Lato,sans-serif;font-size:14px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;border-spacing:0px;width:829px;line-height:1.2857142857;color:rgb(43,43,43)"><tbody style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline"><tr style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline"><td style="border-width:0px 1px 1px 0px;border-style:solid;border-color:rgba(0,0,0,0.0980392);font-family:inherit;font-style:inherit;outline:0px;padding:8px;vertical-align:baseline">Paper Submission (<font color="red" style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">*** deadline extended one week ***</font>):</td><td style="border-width:0px 1px 1px 0px;border-style:solid;border-color:rgba(0,0,0,0.0980392);font-family:inherit;font-style:inherit;outline:0px;padding:8px;vertical-align:baseline"><font color="red" style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">18 Nov 2014</font></td></tr><tr style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline"><td style="border-width:0px 1px 1px 0px;border-style:solid;border-color:rgba(0,0,0,0.0980392);font-family:inherit;font-style:inherit;outline:0px;padding:8px;vertical-align:baseline">Paper Notifications:</td><td style="border-width:0px 1px 1px 0px;border-style:solid;border-color:rgba(0,0,0,0.0980392);font-family:inherit;font-style:inherit;outline:0px;padding:8px;vertical-align:baseline">12 Jan 2015</td></tr><tr style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline"><td style="border-width:0px 1px 1px 0px;border-style:solid;border-color:rgba(0,0,0,0.0980392);font-family:inherit;font-style:inherit;outline:0px;padding:8px;vertical-align:baseline">Camera-ready Papers:</td><td style="border-width:0px 1px 1px 0px;border-style:solid;border-color:rgba(0,0,0,0.0980392);font-family:inherit;font-style:inherit;outline:0px;padding:8px;vertical-align:baseline">9 Feb 2015</td></tr><tr style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline"><td style="border-width:0px 1px 1px 0px;border-style:solid;border-color:rgba(0,0,0,0.0980392);font-family:inherit;font-style:inherit;outline:0px;padding:8px;vertical-align:baseline">Symposium:</td><td style="border-width:0px 1px 1px 0px;border-style:solid;border-color:rgba(0,0,0,0.0980392);font-family:inherit;font-style:inherit;outline:0px;padding:8px;vertical-align:baseline">27 – 29 April 2015</td></tr></tbody></table><h4 style="border:0px;font-family:Lato,sans-serif;font-size:20px;margin:36px 0px 12px;outline:0px;padding:0px;vertical-align:baseline;clear:both;line-height:24px;color:rgb(43,43,43)">LOCATION AND COST</h4><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px">The symposium will take place at the Hilton Hotel, Pasadena, California, USA, April 27-29, 2015.</p><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px">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.</p><h4 style="border:0px;font-family:Lato,sans-serif;font-size:20px;margin:36px 0px 12px;outline:0px;padding:0px;vertical-align:baseline;clear:both;line-height:24px;color:rgb(43,43,43)">SUBMISSION DETAILS</h4><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px">There are two categories of submissions:</p><ol style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px 20px;outline:0px;padding:0px;vertical-align:baseline;list-style-position:initial;color:rgb(43,43,43);line-height:24px"><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Regular papers describing fully developed work and complete results (15 pages)</li><li style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline">Short papers describing tools, experience reports, or descriptions of work in progress with preliminary results (6 pages)</li></ol><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px">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.</p><h4 style="border:0px;font-family:Lato,sans-serif;font-size:20px;margin:36px 0px 12px;outline:0px;padding:0px;vertical-align:baseline;clear:both;line-height:24px;color:rgb(43,43,43)">PC CHAIRS</h4><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px">Klaus Havelund, NASA Jet Propulsion Laboratory, USA<br>Gerard Holzmann, NASA Jet Propulsion Laboratory, USA<br>Rajeev Joshi, NASA Jet Propulsion Laboratory, USA</p><h4 style="border:0px;font-family:Lato,sans-serif;font-size:20px;margin:36px 0px 12px;outline:0px;padding:0px;vertical-align:baseline;clear:both;line-height:24px;color:rgb(43,43,43)">PUBLICITY SUPPORT</h4><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px">Ylies Falcone, Université Joseph Fourier, France</p><h4 style="border:0px;font-family:Lato,sans-serif;font-size:20px;margin:36px 0px 12px;outline:0px;padding:0px;vertical-align:baseline;clear:both;line-height:24px;color:rgb(43,43,43)">PROGRAMME COMMITTEE</h4><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px">Erika Abraham, RWTH Aachen University, Germany<br>Julia Badger, NASA Johnson Space Center, USA<br>Christel Baier, Technische Universität Dresden, Germany<br>Saddek Bensalem, VERIMAG/UJF, France<br>Dirk Beyer, University of Passau, Germany<br>Armin Biere, Johannes Kepler University, Austria<br>Nikolaj Bjorner, Microsoft Research, USA<br>Borzoo Bonakdarpour, McMaster University, Canada<br>Alessandro Cimatti, Fondazione Bruno Kessler, Italy<br>Leonardo de Moura, Microsoft Research, USA<br>Ewen Denney, NASA Ames Research Center, USA<br>Ben Di Vito, NASA Langley Research Center, USA<br>Dawson Engler, Stanford University, USA<br>Jean-Christophe Filliatre, Université Paris-Sud, France<br>Dimitra Giannakopoulou, NASA Ames Research Center, USA<br>Alwyn Goodloe, NASA Langley Research Center, USA<br>Susanne Graf, VERIMAG, France<br>Alex Groce, Oregon State University, USA<br>Radu Grosu, Vienna University of Technology, Austria<br>John Harrison, Intel Corporation, USA<br>Mike Hinchey, University of Limerick/Lero, Ireland<br>Bart Jacobs, University of Leuven, Belgium<br>Sarfraz Khurshid, The University of Texas at Austin, USA<br>Gerwin Klein, NICTA, Australia<br>Daniel Kroening, Oxford University, UK<br>Orna Kupferman, Hebrew University Jerusalem, Israel<br>Kim Larsen, Aalborg University, Denmark<br>Rustan Leino, Microsoft Research, USA<br>Martin Leucker, University of Lubeck, Germany<br>Rupak Majumdar, Max Planck Institute, Germany<br>Pete Manolios, Northeastern University, USA<br>Peter Mueller, ETH Zurich, Switzerland<br>Kedar Namjoshi, Bell Labs/Alcatel-Lucent, USA<br>Corina Pasareanu, NASA Ames Research Center, USA<br>Doron Peled, Bar Ilan University, Israel<br>Suzette Person, NASA Langley Research Center, USA<br>Andreas Podelski, University of Freiburg, Germany<br>Grigore Rosu, University of Illinois, USA<br>Kristin <span style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(0,0,0)">Yvonne </span>Rozier, NASA Ames Research Center, USA<br>Natarajan Shankar, SRI International, USA<br>Natasha Sharygina, University of Lugano, Switzerland<br>Scott Smolka, Stony Brook University, USA<br>Willem Visser, University of Stellenbosch, South Africa<br>Mahesh Viswanathan, University of Illinois, USA<br>Mike Whalen, University of Minnesota, USA<br>Jim Woodcock, University of York, UK</p><h4 style="border:0px;font-family:Lato,sans-serif;font-size:20px;margin:36px 0px 12px;outline:0px;padding:0px;vertical-align:baseline;clear:both;line-height:24px;color:rgb(43,43,43)">STEERING COMMITTEE</h4><p style="border:0px;font-family:Lato,sans-serif;font-size:16px;margin:0px 0px 24px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(43,43,43);line-height:24px">Julia Badger, NASA Johnson Space Center<br>Ewen Denney, NASA Ames Research Center<br>Ben Di Vito, NASA Langley Research Center<br>Klaus Havelund, NASA Jet Propulsion Laboratory<br>Gerard Holzmann, NASA Jet Propulsion Laboratory<br>Cesar Munoz, NASA Langley Research Center<br>Corina Pasareanu, NASA Ames Research Center<br>Suzette Person, NASA Langley Research Center<br>Kristin <span style="border:0px;font-family:inherit;font-style:inherit;margin:0px;outline:0px;padding:0px;vertical-align:baseline;color:rgb(0,0,0)">Yvonne</span> Rozier, NASA Ames Research Center</p></div>