<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"><head><META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=us-ascii"><meta name=Generator content="Microsoft Word 12 (filtered medium)"><style><!--
/* Font Definitions */
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri","sans-serif";}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri","sans-serif";
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]--></head><body lang=EN-US link=blue vlink=purple><div class=WordSection1><p class=MsoNormal>NFM 2012 FIRST CALL FOR PAPERS<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Fourth NASA Formal Methods Symposium<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Norfolk, Virginia, USA<o:p></o:p></p><p class=MsoNormal>April 3 - 5, 2012<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>http://shemesh.larc.nasa.gov/nfm2012/<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>nasa-nfm2012@mail.nasa.gov<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>--------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Theme of Conference:<o:p></o:p></p><p class=MsoNormal>--------------------------------------------------<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>The NASA Formal Methods Symposium is a forum for theoreticians and<o:p></o:p></p><p class=MsoNormal>practitioners from academia, industry, and government, with the goals of<o:p></o:p></p><p class=MsoNormal>identifying challenges and providing solutions to achieving assurance<o:p></o:p></p><p class=MsoNormal>in mission- and safety-critical systems. Within NASA, for example, such <o:p></o:p></p><p class=MsoNormal>systems include autonomous robots, separation assurance algorithms for<o:p></o:p></p><p class=MsoNormal>aircraft, Next Generation Air Transportation (NextGen), and autonomous <o:p></o:p></p><p class=MsoNormal>rendezvous and docking for spacecraft. Moreover, emerging paradigms such <o:p></o:p></p><p class=MsoNormal>as code generation and safety cases are bringing with them new challenges <o:p></o:p></p><p class=MsoNormal>and opportunities. The focus of the symposium will be on formal<o:p></o:p></p><p class=MsoNormal>techniques, their theory, current capabilities, and limitations, as<o:p></o:p></p><p class=MsoNormal>well as their application to aerospace, robotics, and other<o:p></o:p></p><p class=MsoNormal>safety-critical systems. <o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>--------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Topics of Interest:<o:p></o:p></p><p class=MsoNormal>--------------------------------------------------<o:p></o:p></p><p class=MsoNormal>* Formal verification, including theorem proving, model checking,<o:p></o:p></p><p class=MsoNormal> and static analysis<o:p></o:p></p><p class=MsoNormal>* Automated test generation and testing techniques for safety-critical systems<o:p></o:p></p><p class=MsoNormal>* Model-based development<o:p></o:p></p><p class=MsoNormal>* Techniques and algorithms for scaling formal methods, such as abstraction<o:p></o:p></p><p class=MsoNormal> and symbolic methods, compositional techniques, as well as parallel and<o:p></o:p></p><p class=MsoNormal> distributed techniques<o:p></o:p></p><p class=MsoNormal>* Monitoring and runtime verification<o:p></o:p></p><p class=MsoNormal>* Code generation from formally verified models<o:p></o:p></p><p class=MsoNormal>* Significant applications of formal methods to aerospace systems<o:p></o:p></p><p class=MsoNormal>* Modeling and verification aspects of cyber-physical systems<o:p></o:p></p><p class=MsoNormal>* Safety cases<o:p></o:p></p><p class=MsoNormal>* Accident/safety analysis<o:p></o:p></p><p class=MsoNormal>* Formal approaches to fault tolerance<o:p></o:p></p><p class=MsoNormal>* Theoretical advances and empirical evaluations of formal methods<o:p></o:p></p><p class=MsoNormal>* Techniques for safety-critical systems, including hybrid and embedded systems<o:p></o:p></p><p class=MsoNormal>* Formal methods in systems engineering<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>--------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Submissions:<o:p></o:p></p><p class=MsoNormal>--------------------------------------------------<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>There are two categories of submissions:<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>* Regular papers describing fully developed work and complete<o:p></o:p></p><p class=MsoNormal>results (15 pages/30 minute talks)<o:p></o:p></p><p class=MsoNormal>* Short papers describing tools, experience reports, or descriptions of work <o:p></o:p></p><p class=MsoNormal>in progress or?preliminary results (6 pages/15 minute talks)<o:p></o:p></p><p class=MsoNormal>All papers should be in English and describe original work that has not been <o:p></o:p></p><p class=MsoNormal>published or submitted elsewhere. All submissions will be fully reviewed by <o:p></o:p></p><p class=MsoNormal>members of the program committee. Papers must use the LNCS style and be put <o:p></o:p></p><p class=MsoNormal>in PDF format in anticipation that we will publish accepted papers (including<o:p></o:p></p><p class=MsoNormal>regular papers and short papers) in a formal proceedings. Papers should be <o:p></o:p></p><p class=MsoNormal>submitted through the following link: <o:p></o:p></p><p class=MsoNormal>http://www.easychair.org/conferences/?conf=nfm2012 <o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Program Chairs:<o:p></o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Alwyn Goodloe, NASA Langley Research Center<o:p></o:p></p><p class=MsoNormal>Suzette Person, NASA Langley Research Center<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Steering Committee:<o:p></o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Ewen Denney, NASA Ames Research Center<o:p></o:p></p><p class=MsoNormal>Ben Di Vito, NASA Langley Research Center<o:p></o:p></p><p class=MsoNormal>Dimitra Giannakopoulou, NASA Ames Research Center<o:p></o:p></p><p class=MsoNormal>Klaus Havelund, NASA/Jet Propulsion Laboratory<o:p></o:p></p><p class=MsoNormal>Gerard Holzmann, NASA/Jet Propulsion Laboratory<o:p></o:p></p><p class=MsoNormal>Cesar Munoz, NASA Langley Research Center<o:p></o:p></p><p class=MsoNormal>Corina Pasareanu, NASA Ames Research Center<o:p></o:p></p><p class=MsoNormal>James Rash, NASA Goddard<o:p></o:p></p><p class=MsoNormal>Kristin V. Rozier, NASA Ames Research Center<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Important Dates:<o:p></o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Submission: 11 December 2011<o:p></o:p></p><p class=MsoNormal>Notification: 21 January 2012<o:p></o:p></p><p class=MsoNormal>Final Version: 4 February 2012<o:p></o:p></p><p class=MsoNormal>Conference: 3 - 5 April 2012<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Location and Cost:<o:p></o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>The symposium will take place at the Norfolk Waterside Marriott <o:p></o:p></p><p class=MsoNormal>in Norfolk, Virginia, USA. April 3-5, 2012. There will not be a <o:p></o:p></p><p class=MsoNormal>registration fee charged to participants. All interested individuals, <o:p></o:p></p><p class=MsoNormal>including non-US citizens, are welcome to attend, to listen to the talks, <o:p></o:p></p><p class=MsoNormal>and to participate in discussions; however, all attendees must register.<o:p></o:p></p></div></body></html>