<div dir="ltr"><br><div><br></div><div><h3 style="color:rgb(0,0,0);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;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. 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;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></div>