<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div><br></div><div><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;"><font color="#e32400">NFM 2015</font></h3><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 PARTICIPATION</h3><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; -webkit-hyphens: none; line-height: 24px; box-sizing: border-box; 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. 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. The focus of the symposium is on formal methods, and aims to foster collaboration between NASA researchers and engineers and the wider aerospace and academic formal methods communities. </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; list-style-image: 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;">Systematic testing</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</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);">LOCATION, COST, REGISTRATION AND HOTEL ROOM BOOKING</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. </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;">All interested individuals, including non-US citizens, are welcome to attend; however, all attendees must register (but please only register if you intend to attend). Registration form and hotel booking websites are reachable from the main website. A block of rooms at a low price are reserved with booking deadline of March 26.</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></body></html>